|
@@ -112,6 +112,13 @@ const main: JupyterFrontEndPlugin<void> = {
|
|
|
app.commands.notifyCommandChanged();
|
|
|
});
|
|
|
|
|
|
+ // when current tab changes, make sure it is activated
|
|
|
+ app.shell.currentChanged.connect((sender, args) => {
|
|
|
+ if (args.newValue) {
|
|
|
+ app.shell.activateById(args.newValue.id);
|
|
|
+ }
|
|
|
+ });
|
|
|
+
|
|
|
// If the connection to the server is lost, handle it with the
|
|
|
// connection lost handler.
|
|
|
connectionLost = connectionLost || ConnectionLost;
|