Switch to settings for other top bar items

Jeremy Tuloup 4 years ago
parent 7bc2ec6628
commit 1350c66456

@ -0,0 +1,10 @@
{
"title": "Title widget",
"description": "Title widget",
"jupyter.lab.toolbars": {
"TopBar": [{ "name": "widgetTitle", "rank": 10 }]
},
"properties": {},
"additionalProperties": false,
"type": "object"
}

@ -14,7 +14,8 @@ import {
sessionContextDialogs,
ISessionContextDialogs,
DOMUtils,
ICommandPalette
ICommandPalette,
IToolbarWidgetRegistry
} from '@jupyterlab/apputils';
import { ConsolePanel } from '@jupyterlab/console';
@ -390,34 +391,40 @@ const title: JupyterFrontEndPlugin<void> = {
id: '@jupyter-notebook/application-extension:title',
autoStart: true,
requires: [INotebookShell, ITranslator],
optional: [IDocumentManager, IRouter],
optional: [IDocumentManager, IRouter, IToolbarWidgetRegistry],
activate: (
app: JupyterFrontEnd,
shell: INotebookShell,
translator: ITranslator,
docManager: IDocumentManager | null,
router: IRouter | null
router: IRouter | null,
toolbarRegistry: IToolbarWidgetRegistry | null
) => {
const { commands } = app;
const trans = translator.load('notebook');
const widget = new Widget();
widget.id = 'jp-title';
app.shell.add(widget, 'top', { rank: 10 });
const node = document.createElement('div');
if (toolbarRegistry) {
toolbarRegistry.addFactory('TopBar', 'widgetTitle', toolbar => {
const widget = new Widget({ node });
widget.id = 'jp-title';
return widget;
});
}
const addTitle = async (): Promise<void> => {
const current = shell.currentWidget;
if (!current || !(current instanceof DocumentWidget)) {
return;
}
if (widget.node.children.length > 0) {
if (node.children.length > 0) {
return;
}
const h = document.createElement('h1');
h.textContent = current.title.label.replace(STRIP_IPYNB, '');
widget.node.appendChild(h);
widget.node.style.marginLeft = '10px';
node.appendChild(h);
node.style.marginLeft = '10px';
if (!docManager) {
return;
}
@ -465,7 +472,7 @@ const title: JupyterFrontEndPlugin<void> = {
}
});
widget.node.onclick = async () => {
node.onclick = async () => {
void commands.execute(CommandIDs.rename);
};
};

@ -12,3 +12,7 @@
.jp-MainAreaWidget {
height: 100%;
}
.jp-Toolbar > .jp-Toolbar-item {
height: unset;
}

@ -0,0 +1,10 @@
{
"title": "Notebook checkpoint indicator",
"description": "Notebook checkpoint indicator",
"jupyter.lab.toolbars": {
"TopBar": [{ "name": "checkpoint", "rank": 20 }]
},
"properties": {},
"additionalProperties": false,
"type": "object"
}

@ -62,19 +62,26 @@ const checkpoints: JupyterFrontEndPlugin<void> = {
id: '@jupyter-notebook/notebook-extension:checkpoints',
autoStart: true,
requires: [IDocumentManager, ITranslator],
optional: [INotebookShell],
optional: [INotebookShell, IToolbarWidgetRegistry],
activate: (
app: JupyterFrontEnd,
docManager: IDocumentManager,
translator: ITranslator,
notebookShell: INotebookShell | null
notebookShell: INotebookShell | null,
toolbarRegistry: IToolbarWidgetRegistry | null
) => {
const { shell } = app;
const trans = translator.load('notebook');
const widget = new Widget();
widget.id = DOMUtils.createDomID();
widget.addClass('jp-NotebookCheckpoint');
app.shell.add(widget, 'top', { rank: 100 });
const node = document.createElement('div');
if (toolbarRegistry) {
toolbarRegistry.addFactory('TopBar', 'checkpoint', toolbar => {
const widget = new Widget({ node });
widget.id = DOMUtils.createDomID();
widget.addClass('jp-NotebookCheckpoint');
return widget;
});
}
const onChange = async () => {
const current = shell.currentWidget;
@ -91,7 +98,7 @@ const checkpoints: JupyterFrontEndPlugin<void> = {
return;
}
const checkpoint = checkpoints[checkpoints.length - 1];
widget.node.textContent = trans.__(
node.textContent = trans.__(
'Last Checkpoint: %1',
Time.formatHuman(new Date(checkpoint.last_modified))
);

Loading…
Cancel
Save