Merge pull request #75 from jtpio/completer-files

Add the completer-extension:files plugin for editors
jupyterlab · Jan 13, 2021 · 582c850 · 582c850
2 parents 1276f94 + e91083a
commit 582c850
Showing 1 changed file with 7 additions and 4 deletions.
diff --git a/builder/index.js b/builder/index.js
@@ -90,6 +90,9 @@ async function main() {
     require('@jupyterlab/codemirror-extension').default.filter(({ id }) =>
       ['@jupyterlab/codemirror-extension:services'].includes(id)
     ),
+    require('@jupyterlab/completer-extension').default.filter(({ id }) =>
+      ['@jupyterlab/completer-extension:manager'].includes(id)
+    ),
     require('@jupyterlab/docmanager-extension').default.filter(({ id }) =>
       ['@jupyterlab/docmanager-extension:plugin'].includes(id)
     ),
@@ -121,10 +124,7 @@ async function main() {
   } else if (page === 'notebooks') {
     mods = mods.concat([
       require('@jupyterlab/completer-extension').default.filter(({ id }) =>
-        [
-          '@jupyterlab/completer-extension:manager',
-          '@jupyterlab/completer-extension:notebooks'
-        ].includes(id)
+        ['@jupyterlab/completer-extension:notebooks'].includes(id)
       ),
       require('@jupyterlab/tooltip-extension').default.filter(({ id }) =>
         [
@@ -135,6 +135,9 @@ async function main() {
     ]);
   } else if (page === 'edit') {
     mods = mods.concat([
+      require('@jupyterlab/completer-extension').default.filter(({ id }) =>
+        ['@jupyterlab/completer-extension:files'].includes(id)
+      ),
       require('@jupyterlab/fileeditor-extension').default.filter(({ id }) =>
         ['@jupyterlab/fileeditor-extension:plugin'].includes(id)
       ),