mirror/notebook
2
0
Fork 0
mirror of https://github.com/jupyter/notebook.git synced 2025-02-17 12:39:54 +08:00
Code Issues Packages Projects Releases Wiki Activity

Fix top bar visibility not picking up settings overrides (#6833) (#6836)

Browse Source 
* Make 'visible' enum type and pick up both default and user
      settings.
This commit is contained in:
Yanqing Dai 2023-05-03 14:10:20 +08:00 committed by GitHub
parent 7c3c992faf
commit 22b5f14c0a
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 17 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
packages/application-extension/schema/top.json
View File

@ -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,

19
packages/application-extension/src/index.ts
View File

@ -482,22 +482,29 @@ const topVisibility: JupyterFrontEndPlugin<void> = {
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<void> = {
}
const onChanged = (): void => {
if (settingsOverride) {
if (!adjustToScreen) {
return;
}
if (app.format === 'desktop') {