From 18106a006b1fbd59f30b87895f70a20ebf2eb30c Mon Sep 17 00:00:00 2001 From: Jeremy Tuloup Date: Tue, 7 Sep 2021 16:23:49 +0200 Subject: [PATCH] Show path in the console tab title --- packages/application-extension/package.json | 1 + packages/application-extension/src/index.ts | 25 +++++++++++++++------ 2 files changed, 19 insertions(+), 7 deletions(-) diff --git a/packages/application-extension/package.json b/packages/application-extension/package.json index 0e0128d27..7cd173d00 100644 --- a/packages/application-extension/package.json +++ b/packages/application-extension/package.json @@ -44,6 +44,7 @@ "@jupyterlab/celltags": "^3.1.8", "@jupyterlab/codeeditor": "^3.1.8", "@jupyterlab/codemirror": "^3.1.8", + "@jupyterlab/console": "^3.1.8", "@jupyterlab/coreutils": "^5.1.8", "@jupyterlab/docmanager": "^3.1.8", "@jupyterlab/docregistry": "^3.1.8", diff --git a/packages/application-extension/src/index.ts b/packages/application-extension/src/index.ts index 3e2aa5d43..a43f9264a 100644 --- a/packages/application-extension/src/index.ts +++ b/packages/application-extension/src/index.ts @@ -17,6 +17,8 @@ import { ICommandPalette } from '@jupyterlab/apputils'; +import { ConsolePanel } from '@jupyterlab/console'; + import { PageConfig, PathExt, URLExt } from '@jupyterlab/coreutils'; import { IDocumentManager, renameDialog } from '@jupyterlab/docmanager'; @@ -347,15 +349,24 @@ const tabTitle: JupyterFrontEndPlugin = { activate: (app: JupyterFrontEnd, shell: IRetroShell) => { const setTabTitle = () => { const current = shell.currentWidget; - if (!(current instanceof DocumentWidget)) { + if (current instanceof ConsolePanel) { + const update = () => { + const title = + current.sessionContext.path || current.sessionContext.name; + const basename = PathExt.basename(title); + document.title = basename; + }; + current.sessionContext.sessionChanged.connect(update); + update(); return; + } else if (current instanceof DocumentWidget) { + const update = () => { + const basename = PathExt.basename(current.context.path); + document.title = basename; + }; + current.context.pathChanged.connect(update); + update(); } - const update = () => { - const basename = PathExt.basename(current.context.path); - document.title = basename; - }; - current.context.pathChanged.connect(update); - update(); }; shell.currentChanged.connect(setTabTitle);