index.ts 2.2 KB

12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576777879808182838485
  1. /*-----------------------------------------------------------------------------
  2. | Copyright (c) Jupyter Development Team.
  3. | Distributed under the terms of the Modified BSD License.
  4. |----------------------------------------------------------------------------*/
  5. import '../style/settingeditor.css';
  6. import {
  7. ILayoutRestorer, JupyterLab, JupyterLabPlugin
  8. } from '@jupyterlab/application';
  9. import {
  10. InstanceTracker
  11. } from '@jupyterlab/apputils';
  12. import {
  13. IEditorServices
  14. } from '@jupyterlab/codeeditor';
  15. import {
  16. ISettingRegistry, IStateDB
  17. } from '@jupyterlab/coreutils';
  18. import {
  19. SettingEditor
  20. } from './settingeditor';
  21. /**
  22. * The command IDs used by the setting editor.
  23. */
  24. namespace CommandIDs {
  25. export
  26. const open = 'settingeditor:open';
  27. }
  28. /**
  29. * The default setting editor extension.
  30. */
  31. const plugin: JupyterLabPlugin<void> = {
  32. id: '@jupyterlab/settingeditor-extension:plugin',
  33. activate: (app: JupyterLab, restorer: ILayoutRestorer, registry: ISettingRegistry, editorServices: IEditorServices, state: IStateDB) => {
  34. const { commands, shell } = app;
  35. const namespace = 'setting-editor';
  36. const factoryService = editorServices.factoryService;
  37. const editorFactory = factoryService.newInlineEditor.bind(factoryService);
  38. const tracker = new InstanceTracker<SettingEditor>({ namespace });
  39. // Handle state restoration.
  40. restorer.restore(tracker, {
  41. command: CommandIDs.open,
  42. args: widget => ({ }),
  43. name: widget => namespace
  44. });
  45. commands.addCommand(CommandIDs.open, {
  46. execute: () => {
  47. if (tracker.currentWidget) {
  48. shell.activateById(tracker.currentWidget.id);
  49. return;
  50. }
  51. const key = plugin.id;
  52. const when = app.restored;
  53. const editor = new SettingEditor({
  54. editorFactory, key, registry, state, when
  55. });
  56. tracker.add(editor);
  57. editor.id = namespace;
  58. editor.title.label = 'Settings';
  59. editor.title.iconClass = 'jp-SettingsIcon';
  60. editor.title.closable = true;
  61. shell.addToMainArea(editor);
  62. shell.activateById(editor.id);
  63. },
  64. label: 'Settings'
  65. });
  66. },
  67. requires: [ILayoutRestorer, ISettingRegistry, IEditorServices, IStateDB],
  68. autoStart: true
  69. };
  70. export default plugin;