Merge pull request #5570 from AlbertHilb/TerminalSettings

Add terminal section to settings editor.

packages/terminal-extension/package.json

@@ -32,6 +32,7 @@
   "dependencies": {
     "@jupyterlab/application": "^0.19.1",
     "@jupyterlab/apputils": "^0.19.1",
+    "@jupyterlab/coreutils": "^2.2.1",
     "@jupyterlab/launcher": "^0.19.1",
     "@jupyterlab/mainmenu": "^0.8.1",
     "@jupyterlab/services": "^3.2.1",
@@ -46,6 +47,7 @@
     "access": "public"
   },
   "jupyterlab": {
-    "extension": true
+    "extension": true,
+    "schemaDir": "schema"
   }
 }

packages/terminal-extension/schema/plugin.json

@@ -0,0 +1,51 @@
+{
+  "jupyter.lab.setting-icon-class": "jp-TerminalIcon",
+  "jupyter.lab.setting-icon-label": "Terminal",
+  "title": "Terminal",
+  "description": "Terminal settings.",
+  "definitions": {
+    "fontFamily": {
+      "type": "string"
+    },
+    "fontSize": {
+      "type": "integer",
+      "minimum": 9,
+      "maximum": 72
+    },
+    "lineHeight": {
+      "type": "number",
+      "minimum": 1.0
+    },
+    "theme": {
+      "enum": ["dark", "light"]
+    }
+  },
+  "properties": {
+    "fontFamily": {
+      "title": "Font family",
+      "description": "The font family used to render text.",
+      "$ref": "#/definitions/fontFamily",
+      "default": "courier-new, courier, monospace"
+    },
+    "fontSize": {
+      "title": "Font size",
+      "description": "The font size used to render text.",
+      "$ref": "#/definitions/fontSize",
+      "default": 13
+    },
+    "lineHeight": {
+      "title": "Line height",
+      "description": "The line height used to render text.",
+      "$ref": "#/definitions/lineHeight",
+      "default": 1.0
+    },
+    "theme": {
+      "title": "Theme",
+      "description": "The theme for the terminal.",
+      "$ref": "#/definitions/theme",
+      "default": "dark"
+    }
+  },
+  "additionalProperties": false,
+  "type": "object"
+}

packages/terminal-extension/src/index.ts

@@ -21,6 +21,8 @@ import { ServiceManager } from '@jupyterlab/services';
 
 import { ITerminalTracker, Terminal } from '@jupyterlab/terminal';
 
+import { ISettingRegistry } from '@jupyterlab/coreutils';
+
 /**
  * The command IDs used by the terminal plugin.
  */
@@ -50,7 +52,7 @@ const plugin: JupyterLabPlugin<ITerminalTracker> = {
   activate,
   id: '@jupyterlab/terminal-extension:plugin',
   provides: ITerminalTracker,
-  requires: [IMainMenu, ICommandPalette, ILayoutRestorer],
+  requires: [IMainMenu, ICommandPalette, ILayoutRestorer, ISettingRegistry],
   optional: [ILauncher],
   autoStart: true
 };
@@ -68,6 +70,7 @@ function activate(
   mainMenu: IMainMenu,
   palette: ICommandPalette,
   restorer: ILayoutRestorer,
+  settingRegistry: ISettingRegistry,
   launcher: ILauncher | null
 ): ITerminalTracker {
   const { serviceManager } = app;
@@ -90,7 +93,55 @@ function activate(
     name: widget => widget.content.session && widget.content.session.name
   });
 
-  addCommands(app, serviceManager, tracker);
+  // The terminal options from the setting editor.
+  let options: Partial<Terminal.IOptions>;
+
+  /**
+   * Update the option values.
+   */
+  function updateOptions(settings: ISettingRegistry.ISettings): void {
+    options = settings.composite as Partial<Terminal.IOptions>;
+    Object.keys(options).forEach((key: keyof Terminal.IOptions) => {
+      Terminal.defaultOptions[key] = options[key];
+    });
+  }
+
+  /**
+   * Update terminal
+   */
+  function updateTerminal(widget: MainAreaWidget<Terminal>): void {
+    const terminal = widget.content;
+    if (!terminal) {
+      return;
+    }
+    Object.keys(options).forEach((key: keyof Terminal.IOptions) => {
+      terminal.setOption(key, options[key]);
+    });
+  }
+
+  /**
+   * Update the settings of the current tracker instances.
+   */
+  function updateTracker(): void {
+    tracker.forEach(widget => updateTerminal(widget));
+  }
+
+  // Fetch the initial state of the settings.
+  settingRegistry
+    .load(plugin.id)
+    .then(settings => {
+      updateOptions(settings);
+      updateTracker();
+      settings.changed.connect(() => {
+        updateOptions(settings);
+        updateTracker();
+      });
+    })
+    .catch((reason: Error) => {
+      console.error(reason.message);
+    });
+
+  addCommands(app, serviceManager, tracker, settingRegistry);
 
   // Add some commands to the application view menu.
   const viewGroup = [
@@ -100,7 +151,7 @@ function activate(
   ].map(command => {
     return { command };
   });
-  mainMenu.viewMenu.addGroup(viewGroup, 30);
+  mainMenu.settingsMenu.addGroup(viewGroup, 40);
 
   // Add command palette items.
   [
@@ -140,20 +191,11 @@ function activate(
 export function addCommands(
   app: JupyterLab,
   services: ServiceManager,
-  tracker: InstanceTracker<MainAreaWidget<Terminal>>
+  tracker: InstanceTracker<MainAreaWidget<Terminal>>,
+  settingRegistry: ISettingRegistry
 ) {
   let { commands, shell } = app;
 
-  /**
-   * Whether there is an active terminal.
-   */
-  function isEnabled(): boolean {
-    return (
-      tracker.currentWidget !== null &&
-      tracker.currentWidget === app.shell.currentWidget
-    );
-  }
-
   // Add terminal commands.
   commands.addCommand(CommandIDs.createNew, {
     label: args => (args['isPalette'] ? 'New Terminal' : 'Terminal'),
@@ -222,50 +264,45 @@ export function addCommands(
     isEnabled: () => tracker.currentWidget !== null
   });
 
+  function showErrorMessage(error: Error): void {
+    console.error(`Failed to set ${plugin.id}: ${error.message}`);
+  }
+
   commands.addCommand(CommandIDs.increaseFont, {
     label: 'Increase Terminal Font Size',
     execute: () => {
-      let options = Terminal.defaultOptions;
-      if (options.fontSize < 72) {
-        options.fontSize++;
-        tracker.forEach(widget => {
-          widget.content.fontSize = options.fontSize;
-        });
+      let { fontSize } = Terminal.defaultOptions;
+      if (fontSize < 72) {
+        return settingRegistry
+          .set(plugin.id, 'fontSize', fontSize + 1)
+          .catch(showErrorMessage);
       }
-    },
-    isEnabled
+    }
   });
 
   commands.addCommand(CommandIDs.decreaseFont, {
     label: 'Decrease Terminal Font Size',
     execute: () => {
-      let options = Terminal.defaultOptions;
-      if (options.fontSize > 9) {
-        options.fontSize--;
-        tracker.forEach(widget => {
-          widget.content.fontSize = options.fontSize;
-        });
+      let { fontSize } = Terminal.defaultOptions;
+      if (fontSize > 9) {
+        return settingRegistry
+          .set(plugin.id, 'fontSize', fontSize - 1)
+          .catch(showErrorMessage);
       }
-    },
-    isEnabled
+    }
   });
 
-  let terminalTheme: Terminal.Theme = 'dark';
   commands.addCommand(CommandIDs.toggleTheme, {
     label: 'Use Dark Terminal Theme',
     caption: 'Whether to use the dark terminal theme',
-    isToggled: () => terminalTheme === 'dark',
+    isToggled: () => Terminal.defaultOptions.theme === 'dark',
     execute: () => {
-      terminalTheme = terminalTheme === 'dark' ? 'light' : 'dark';
-      let options = Terminal.defaultOptions;
-      options.theme = terminalTheme;
-      tracker.forEach(widget => {
-        if (widget.content.theme !== terminalTheme) {
-          widget.content.theme = terminalTheme;
-        }
-      });
-      commands.notifyCommandChanged(CommandIDs.toggleTheme);
-    },
-    isEnabled
+      let { theme } = Terminal.defaultOptions;
+      theme = theme === 'dark' ? 'light' : 'dark';
+      return settingRegistry
+        .set(plugin.id, 'theme', theme)
+        .then(() => commands.notifyCommandChanged(CommandIDs.toggleTheme))
+        .catch(showErrorMessage);
+    }
   });
 }

packages/terminal-extension/tsconfig.json

@@ -12,6 +12,9 @@
     {
       "path": "../apputils"
     },
+    {
+      "path": "../coreutils"
+    },
     {
       "path": "../launcher"
     },

packages/terminal/src/widget.ts

@@ -7,7 +7,7 @@ import { Message, MessageLoop } from '@phosphor/messaging';
 
 import { Widget } from '@phosphor/widgets';
 
-import { Terminal as Xterm, ITerminalOptions as IXtermOptions } from 'xterm';
+import { Terminal as Xterm } from 'xterm';
 
 import { fit } from 'xterm/lib/addons/fit';
 
@@ -32,17 +32,24 @@ export class Terminal extends Widget {
    */
   constructor(options: Partial<Terminal.IOptions> = {}) {
     super();
+
+    // Initialize settings.
+    this._options = { ...Terminal.defaultOptions, ...options };
+
+    const { initialCommand, theme, ...other } = this._options;
+    const { lightTheme, darkTheme } = Private;
+    const xtermTheme = theme === 'light' ? lightTheme : darkTheme;
+    const xtermOptions = { theme: xtermTheme, ...other };
+
     this.addClass(TERMINAL_CLASS);
+    if (theme === 'light') {
+      this.addClass('jp-mod-light');
+    }
 
     // Create the xterm.
-    this._term = new Xterm(Private.getConfig(options));
+    this._term = new Xterm(xtermOptions);
     this._initializeTerm();
 
-    // Initialize settings.
-    let defaults = Terminal.defaultOptions;
-    this._initialCommand = options.initialCommand || defaults.initialCommand;
-    this.theme = options.theme || defaults.theme;
-
     this.id = `jp-Terminal-${Private.id++}`;
     this.title.label = 'Terminal';
   }
@@ -71,53 +78,54 @@ export class Terminal extends Widget {
       );
       this.title.label = `Terminal ${value.name}`;
       this._setSessionSize();
-      if (this._initialCommand) {
+      if (this._options.initialCommand) {
         this._session.send({
           type: 'stdin',
-          content: [this._initialCommand + '\r']
+          content: [this._options.initialCommand + '\r']
         });
       }
     });
   }
 
   /**
-   * Get the font size of the terminal in pixels.
+   * Set a config option for the terminal.
    */
-  get fontSize(): number {
-    return this._term.getOption('fontSize');
+  getOption<K extends keyof Terminal.IOptions>(
+    option: K
+  ): Terminal.IOptions[K] {
+    return this._options[option];
   }
 
   /**
-   * Set the font size of the terminal in pixels.
+   * Set a config option for the terminal.
    */
-  set fontSize(size: number) {
-    if (this.fontSize === size) {
+  setOption<K extends keyof Terminal.IOptions>(
+    option: K,
+    value: Terminal.IOptions[K]
+  ): void {
+    if (this._options[option] === value) {
       return;
     }
-    this._term.setOption('fontSize', size);
-    this._needsResize = true;
-    this.update();
-  }
 
-  /**
-   * Get the current theme, either light or dark.
-   */
-  get theme(): Terminal.Theme {
-    return this._theme;
-  }
+    this._options[option] = value;
 
-  /**
-   * Set the current theme, either light or dark.
-   */
-  set theme(value: Terminal.Theme) {
-    this._theme = value;
-    if (value === 'light') {
-      this.addClass('jp-mod-light');
-      this._term.setOption('theme', Private.lightTheme);
+    if (option === 'initialCommand') {
+      return;
+    }
+
+    if (option === 'theme') {
+      if (value === 'light') {
+        this.addClass('jp-mod-light');
+        this._term.setOption('theme', Private.lightTheme);
+      } else {
+        this.removeClass('jp-mod-light');
+        this._term.setOption('theme', Private.darkTheme);
+      }
     } else {
-      this.removeClass('jp-mod-light');
-      this._term.setOption('theme', Private.darkTheme);
+      this._term.setOption(option, value);
+      this._needsResize = true;
     }
+
     this.update();
   }
 
@@ -290,12 +298,11 @@ export class Terminal extends Widget {
 
   private _term: Xterm;
   private _needsResize = true;
-  private _theme: Terminal.Theme = 'dark';
   private _session: TerminalSession.ISession | null = null;
-  private _initialCommand: string;
   private _termOpened = false;
   private _offsetWidth = -1;
   private _offsetHeight = -1;
+  private _options: Terminal.IOptions;
 }
 
 /**
@@ -306,11 +313,21 @@ export namespace Terminal {
    * Options for the terminal widget.
    */
   export interface IOptions {
+    /**
+     * The font family used to render text.
+     */
+    fontFamily: string | null;
+
     /**
      * The font size of the terminal in pixels.
      */
     fontSize: number;
 
+    /**
+     * The line height used to render text.
+     */
+    lineHeight: number | null;
+
     /**
      * The theme of the terminal.
      */
@@ -332,7 +349,9 @@ export namespace Terminal {
    */
   export const defaultOptions: IOptions = {
     theme: 'dark',
+    fontFamily: 'courier-new, courier, monospace',
     fontSize: 13,
+    lineHeight: 1.0,
     cursorBlink: true,
     initialCommand: ''
   };
@@ -347,26 +366,6 @@ export namespace Terminal {
  * A namespace for private data.
  */
 namespace Private {
-  /**
-   * Get term.js options from ITerminalOptions.
-   */
-  export function getConfig(
-    options: Partial<Terminal.IOptions>
-  ): IXtermOptions {
-    let config: IXtermOptions = {};
-    if (options.cursorBlink !== void 0) {
-      config.cursorBlink = options.cursorBlink;
-    } else {
-      config.cursorBlink = Terminal.defaultOptions.cursorBlink;
-    }
-    if (options.fontSize !== void 0) {
-      config.fontSize = options.fontSize;
-    } else {
-      config.fontSize = Terminal.defaultOptions.fontSize;
-    }
-    return config;
-  }
-
   /**
    * An incrementing counter for ids.
    */

tests/test-terminal/src/terminal.spec.ts

@@ -87,12 +87,12 @@ describe('terminal/index', () => {
 
     describe('#fontSize', () => {
       it('should be 13 by default', () => {
-        expect(widget.fontSize).to.equal(13);
+        expect(widget.getOption('fontSize')).to.equal(13);
       });
 
       it('should trigger an update request', async () => {
-        widget.fontSize = 14;
-        expect(widget.fontSize).to.equal(14);
+        widget.setOption('fontSize', 14);
+        expect(widget.getOption('fontSize')).to.equal(14);
         await framePromise();
         expect(widget.methods).to.contain('onUpdateRequest');
       });
@@ -100,12 +100,12 @@ describe('terminal/index', () => {
 
     describe('#theme', () => {
       it('should be dark by default', () => {
-        expect(widget.theme).to.equal('dark');
+        expect(widget.getOption('theme')).to.equal('dark');
       });
 
       it('should be light if we change it', () => {
-        widget.theme = 'light';
-        expect(widget.theme).to.equal('light');
+        widget.setOption('theme', 'light');
+        expect(widget.getOption('theme')).to.equal('light');
       });
     });