|
@@ -237,10 +237,12 @@ async function activateConsole(
|
|
|
...(options as Partial<ConsolePanel.IOptions>)
|
|
|
});
|
|
|
|
|
|
- const interactionMode: string = (await settingRegistry.get(
|
|
|
- '@jupyterlab/console-extension:tracker',
|
|
|
- 'interactionMode'
|
|
|
- )).composite as string;
|
|
|
+ const interactionMode: string = (
|
|
|
+ await settingRegistry.get(
|
|
|
+ '@jupyterlab/console-extension:tracker',
|
|
|
+ 'interactionMode'
|
|
|
+ )
|
|
|
+ ).composite as string;
|
|
|
panel.console.node.dataset.jpInteractionMode = interactionMode;
|
|
|
|
|
|
// Add the console panel to the tracker. We want the panel to show up before
|
|
@@ -580,9 +582,11 @@ async function activateConsole(
|
|
|
execute: async args => {
|
|
|
const key = 'keyMap';
|
|
|
try {
|
|
|
- await settingRegistry.set(pluginId, 'interactionMode', args[
|
|
|
- 'interactionMode'
|
|
|
- ] as string);
|
|
|
+ await settingRegistry.set(
|
|
|
+ pluginId,
|
|
|
+ 'interactionMode',
|
|
|
+ args['interactionMode'] as string
|
|
|
+ );
|
|
|
} catch (reason) {
|
|
|
console.error(`Failed to set ${pluginId}:${key} - ${reason.message}`);
|
|
|
}
|