|
@@ -5,6 +5,10 @@ import {
|
|
JupyterLab, JupyterLabPlugin
|
|
JupyterLab, JupyterLabPlugin
|
|
} from '@jupyterlab/application';
|
|
} from '@jupyterlab/application';
|
|
|
|
|
|
|
|
+import {
|
|
|
|
+ each
|
|
|
|
+} from '@phosphor/algorithm';
|
|
|
|
+
|
|
import {
|
|
import {
|
|
TabBar
|
|
TabBar
|
|
} from '@phosphor/widgets';
|
|
} from '@phosphor/widgets';
|
|
@@ -17,9 +21,14 @@ const plugin: JupyterLabPlugin<void> = {
|
|
id: 'jupyter.extensions.tab-manager',
|
|
id: 'jupyter.extensions.tab-manager',
|
|
activate: (app: JupyterLab): void => {
|
|
activate: (app: JupyterLab): void => {
|
|
const tabs = new TabBar({ orientation: 'vertical' });
|
|
const tabs = new TabBar({ orientation: 'vertical' });
|
|
|
|
+ const populate = () => {
|
|
|
|
+ each(app.shell.widgets('main'), widget => { tabs.addTab(widget.title); });
|
|
|
|
+ };
|
|
|
|
|
|
tabs.id = 'tab-manager';
|
|
tabs.id = 'tab-manager';
|
|
tabs.title.label = 'Tabs';
|
|
tabs.title.label = 'Tabs';
|
|
|
|
+ populate();
|
|
|
|
+ app.shell.currentChanged.connect(populate);
|
|
app.shell.addToLeftArea(tabs, { rank: 600 });
|
|
app.shell.addToLeftArea(tabs, { rank: 600 });
|
|
},
|
|
},
|
|
autoStart: true
|
|
autoStart: true
|