Browse Source

Add header.

Afshin Darian 8 years ago
parent
commit
c30cbc542c

+ 8 - 4
packages/tabmanager-extension/src/index.ts

@@ -26,17 +26,21 @@ const plugin: JupyterLabPlugin<void> = {
   activate: (app: JupyterLab, restorer: ILayoutRestorer): void => {
     const { shell } = app;
     const tabs = new TabBar<Widget>({ orientation: 'vertical' });
-    const populate = () => {
-      tabs.clearTabs();
-      each(shell.widgets('main'), widget => { tabs.addTab(widget.title); });
-    };
+    const header = document.createElement('header');
 
     restorer.add(tabs, 'tab-manager');
     tabs.id = 'tab-manager';
     tabs.title.label = 'Tabs';
+    header.textContent = 'Open Tabs';
+    tabs.node.insertBefore(header, tabs.contentNode);
     shell.addToLeftArea(tabs, { rank: 600 });
 
     app.restored.then(() => {
+      const populate = () => {
+        tabs.clearTabs();
+        each(shell.widgets('main'), widget => { tabs.addTab(widget.title); });
+      };
+
       // Connect signal handlers.
       shell.layoutModified.connect(() => { populate(); });
       tabs.tabActivateRequested.connect((sender, tab) => {

+ 13 - 1
packages/tabmanager-extension/style/index.css

@@ -26,6 +26,18 @@
 }
 
 
+#tab-manager header {
+  border-bottom: var(--jp-border-width) solid var(--jp-border-color2);
+  flex: 0 0 auto;
+  font-size: var(--jp-ui-font-size0);
+  font-weight: 600;
+  letter-spacing: 1px;
+  margin: 4px 0px;
+  padding: 4px 12px;
+  text-transform: uppercase;
+}
+
+
 #tab-manager .p-TabBar-tab {
   margin-left: calc(-1*var(--jp-border-width));
   height: var(--jp-private-tab-manager-tab-height);
@@ -79,7 +91,7 @@
 
 #tab-manager .p-TabBar-tab.p-mod-closable > .p-TabBar-tabCloseIcon {
   margin-left: 4px;
-  padding-top: 10px;
+  padding-top: 12px;
   background-size: 16px;
   height: 16px;
   width: 16px;