From 22b5f14c0a923aff5e5bb4156e084b343290bfa6 Mon Sep 17 00:00:00 2001 From: Yanqing Dai Date: Wed, 3 May 2023 14:10:20 +0800 Subject: [PATCH] Fix top bar visibility not picking up settings overrides (#6833) (#6836) * Make 'visible' enum type and pick up both default and user settings. --- .../application-extension/schema/top.json | 7 ++++--- packages/application-extension/src/index.ts | 19 +++++++++++++------ 2 files changed, 17 insertions(+), 9 deletions(-) diff --git a/packages/application-extension/schema/top.json b/packages/application-extension/schema/top.json index 92c7c1d36..dafe4b799 100644 --- a/packages/application-extension/schema/top.json +++ b/packages/application-extension/schema/top.json @@ -18,10 +18,11 @@ }, "properties": { "visible": { - "type": "boolean", + "type": "string", + "enum": ["yes", "no", "automatic"], "title": "Top Bar Visibility", - "description": "Whether to show the top bar or not", - "default": true + "description": "Whether to show the top bar or not, yes for always showing, no for always not showing, automatic for adjusting to screen size", + "default": "automatic" } }, "additionalProperties": false, diff --git a/packages/application-extension/src/index.ts b/packages/application-extension/src/index.ts index 1438d1f8e..9ec56faed 100644 --- a/packages/application-extension/src/index.ts +++ b/packages/application-extension/src/index.ts @@ -482,22 +482,29 @@ const topVisibility: JupyterFrontEndPlugin = { execute: () => { top.setHidden(top.isVisible); if (settingRegistry) { - void settingRegistry.set(pluginId, 'visible', top.isVisible); + void settingRegistry.set( + pluginId, + 'visible', + top.isVisible ? 'yes' : 'no' + ); } }, isToggled: () => top.isVisible, }); - let settingsOverride = false; + let adjustToScreen = false; if (settingRegistry) { const loadSettings = settingRegistry.load(pluginId); const updateSettings = (settings: ISettingRegistry.ISettings): void => { - const visible = settings.get('visible').composite; + // 'visible' property from user preferences or default settings + let visible = settings.get('visible').composite; if (settings.user.visible !== undefined) { - settingsOverride = true; - top.setHidden(!visible); + visible = settings.user.visible; } + top.setHidden(visible === 'no'); + // adjust to screen from user preferences or default settings + adjustToScreen = visible === 'automatic'; }; Promise.all([loadSettings, app.restored]) @@ -517,7 +524,7 @@ const topVisibility: JupyterFrontEndPlugin = { } const onChanged = (): void => { - if (settingsOverride) { + if (!adjustToScreen) { return; } if (app.format === 'desktop') {