From 010a20befacd25f161a5b896ed9ffb7f3c85b59b Mon Sep 17 00:00:00 2001 From: Jeremy Tuloup Date: Fri, 20 May 2022 17:23:17 +0200 Subject: [PATCH] Fix search provider --- app/index.js | 11 +++++++++-- packages/documentsearch-extension/src/index.ts | 6 ++---- 2 files changed, 11 insertions(+), 6 deletions(-) diff --git a/app/index.js b/app/index.js index 91cbff4d7..0e51804b6 100644 --- a/app/index.js +++ b/app/index.js @@ -163,6 +163,7 @@ async function main() { '@jupyterlab/filebrowser-extension:download', '@jupyterlab/filebrowser-extension:file-upload-status', '@jupyterlab/filebrowser-extension:open-with', + '@jupyterlab/filebrowser-extension:search', '@jupyterlab/filebrowser-extension:share-file' ].includes(id) ), @@ -175,7 +176,10 @@ async function main() { baseMods = baseMods.concat([ require('@jupyterlab/cell-toolbar-extension'), require('@jupyterlab/notebook-extension').default.filter(({ id }) => - ['@jupyterlab/notebook-extension:completer'].includes(id) + [ + '@jupyterlab/notebook-extension:completer', + '@jupyterlab/notebook-extension:search' + ].includes(id) ), require('@jupyterlab/tooltip-extension').default.filter(({ id }) => [ @@ -203,7 +207,10 @@ async function main() { ['@jupyterlab/codemirror-extension:commands'].includes(id) ), require('@jupyterlab/fileeditor-extension').default.filter(({ id }) => - ['@jupyterlab/fileeditor-extension:completer'].includes(id) + [ + '@jupyterlab/fileeditor-extension:completer', + '@jupyterlab/fileeditor-extension:search' + ].includes(id) ), require('@jupyterlab/filebrowser-extension').default.filter(({ id }) => ['@jupyterlab/filebrowser-extension:browser'].includes(id) diff --git a/packages/documentsearch-extension/src/index.ts b/packages/documentsearch-extension/src/index.ts index 6a42df5f6..400d3c0e4 100644 --- a/packages/documentsearch-extension/src/index.ts +++ b/packages/documentsearch-extension/src/index.ts @@ -29,11 +29,9 @@ const notebookShellWidgetListener: JupyterFrontEndPlugin = { if (!widget) { return; } - const providerForWidget = registry.getProvider(widget); - if (providerForWidget) { + if (registry.hasProvider(widget)) { widget.addClass(SEARCHABLE_CLASS); - } - if (!providerForWidget) { + } else { widget.removeClass(SEARCHABLE_CLASS); } };