mirror/notebook
2
0
Fork 0
mirror of https://github.com/jupyter/notebook.git synced 2024-11-27 03:20:27 +08:00
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #6415 from jeewonkoo/develop

Browse Source 
add the show header command to the command palette
This commit is contained in:
Jeremy Tuloup 2022-05-03 10:26:55 +02:00 committed by GitHub
commit 9cde2b6ed8
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 7 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -481,12 +481,13 @@ const title: JupyterFrontEndPlugin<void> = {
const topVisibility: JupyterFrontEndPlugin<void> = {
id: '@jupyter-notebook/application-extension:top',
requires: [INotebookShell, ITranslator],
optional: [ISettingRegistry],
optional: [ISettingRegistry, ICommandPalette],
activate: (
app: JupyterFrontEnd<JupyterFrontEnd.IShell>,
notebookShell: INotebookShell,
translator: ITranslator,
settingRegistry: ISettingRegistry | null
settingRegistry: ISettingRegistry | null,
palette: ICommandPalette | null
) => {
const trans = translator.load('notebook');
const top = notebookShell.top;
@ -527,6 +528,10 @@ const topVisibility: JupyterFrontEndPlugin<void> = {
});
}
if (palette) {
palette.addItem({ command: CommandIDs.toggleTop, category: 'View' });
}
const onChanged = (): void => {
if (settingsOverride) {
return;