Merge pull request #4673 from AlbertHilb/FontSetting

Add `fontFamily` and `fontSize` to CodeEditor configuration.

packages/codeeditor/src/editor.ts

@@ -561,6 +561,21 @@ namespace CodeEditor {
    */
   export
   interface IConfig {
+    /**
+     * User preferred font family for text editors.
+     */
+    fontFamily: string | null;
+
+    /**
+     * User preferred size in pixel of the font used in text editors.
+     */
+    fontSize: number | null;
+
+    /**
+     * User preferred text line height, as a multiplier of font size.
+     */
+    lineHeight: number | null;
+
     /**
      * Whether line numbers should be displayed.
      */
@@ -602,6 +617,9 @@ namespace CodeEditor {
    */
   export
   let defaultConfig: IConfig = {
+    fontFamily: null,
+    fontSize: null,
+    lineHeight: null,
     lineNumbers: false,
     lineWrap: true,
     readOnly: false,

packages/codemirror/src/editor.ts

@@ -112,8 +112,12 @@ class CodeMirrorEditor implements CodeEditor.IEditor {
     };
 
     let model = this._model = options.model;
-    let editor = this._editor = CodeMirror(host, {});
-    Private.handleConfig(editor, options.config || {});
+    let config = options.config || {};
+    let fullConfig = this._config = {
+      ...CodeMirrorEditor.defaultConfig,
+      ...config
+    };
+    let editor = this._editor = Private.createEditor(host, fullConfig);
 
     let doc = editor.getDoc();
 
@@ -260,14 +264,18 @@ class CodeMirrorEditor implements CodeEditor.IEditor {
    * Get a config option for the editor.
    */
   getOption<K extends keyof CodeMirrorEditor.IConfig>(option: K): CodeMirrorEditor.IConfig[K] {
-    return Private.getOption(this.editor, option);
+    return this._config[option];
   }
 
   /**
    * Set a config option for the editor.
    */
   setOption<K extends keyof CodeMirrorEditor.IConfig>(option: K, value: CodeMirrorEditor.IConfig[K]): void {
-    Private.setOption(this.editor, option, value);
+    // Don't bother setting the option if it is already the same.
+    if (this._config[option] !== value) {
+      this._config[option] = value;
+      Private.setOption(this.editor, option, value);
+    }
   }
 
   /**
@@ -897,6 +905,7 @@ class CodeMirrorEditor implements CodeEditor.IEditor {
   private _editor: CodeMirror.Editor;
   protected selectionMarkers: { [key: string]: CodeMirror.TextMarker[] | undefined } = {};
   private _caretHover: HTMLElement | null;
+  private readonly _config: CodeMirrorEditor.IConfig;
   private _hoverTimeout: number;
   private _hoverId: string;
   private _keydownHandlers = new Array<CodeEditor.KeydownHandler>();
@@ -980,7 +989,7 @@ namespace CodeMirrorEditor {
      * (it will default to be to the right of all other gutters).
      * These class names are the keys passed to setGutterMarker.
      */
-    gutters?: ReadonlyArray<string>;
+    gutters?: string[];
 
     /**
      * Determines whether the gutter scrolls along with the content
@@ -1050,7 +1059,7 @@ namespace CodeMirrorEditor {
     electricChars: true,
     keyMap: 'default',
     extraKeys: null,
-    gutters: Object.freeze([]),
+    gutters: [],
     fixedGutter: true,
     showCursorWhenSelecting: false,
     coverGutterNextToScrollbar: false,
@@ -1079,19 +1088,42 @@ namespace CodeMirrorEditor {
  * The namespace for module private data.
  */
 namespace Private {
-  /**
-   * Handle the codemirror configuration options.
-   */
   export
-  function handleConfig(editor: CodeMirror.Editor, config: Partial<CodeMirrorEditor.IConfig>): void {
-    let fullConfig: CodeMirrorEditor.IConfig = {
-      ...CodeMirrorEditor.defaultConfig,
-      ...config
+  function createEditor(host: HTMLElement, config: CodeMirrorEditor.IConfig): CodeMirror.Editor {
+    let {
+      autoClosingBrackets,
+      fontFamily,
+      fontSize,
+      insertSpaces,
+      lineHeight,
+      lineWrap,
+      tabSize,
+      readOnly,
+      ...otherOptions
+    } = config;
+    let bareConfig =  {
+      autoCloseBrackets: autoClosingBrackets,
+      indentUnit: tabSize,
+      indentWithTabs: !insertSpaces,
+      lineWrapping: lineWrap,
+      readOnly,
+      ...otherOptions
     };
-    let key: keyof CodeMirrorEditor.IConfig;
-    for (key in fullConfig) {
-      Private.setOption(editor, key, fullConfig[key]);
-    }
+    return CodeMirror(el => {
+      if (fontFamily) {
+        el.style.fontFamily = fontFamily;
+      }
+      if (fontSize) {
+        el.style.fontSize = fontSize + 'px';
+      }
+      if (lineHeight) {
+        el.style.lineHeight = lineHeight.toString();
+      }
+      if (readOnly) {
+        el.classList.add(READ_ONLY_CLASS);
+      }
+      host.appendChild(el);
+    }, bareConfig);
   }
 
   /**
@@ -1155,35 +1187,12 @@ namespace Private {
     return a.line === b.line && a.ch === b.ch;
   }
 
-  /**
-   * Get a config option for the editor.
-   */
-  export
-  function getOption<K extends keyof CodeMirrorEditor.IConfig>(editor: CodeMirror.Editor, option: K): CodeMirrorEditor.IConfig[K] {
-    switch (option) {
-    case 'lineWrap':
-      return editor.getOption('lineWrapping');
-    case 'insertSpaces':
-      return !editor.getOption('indentWithTabs');
-    case 'tabSize':
-      return editor.getOption('indentUnit');
-    case 'autoClosingBrackets':
-      return editor.getOption('autoCloseBrackets');
-    default:
-      return editor.getOption(option);
-    }
-  }
-
   /**
    * Set a config option for the editor.
    */
   export
   function setOption<K extends keyof CodeMirrorEditor.IConfig>(editor: CodeMirror.Editor, option: K, value: CodeMirrorEditor.IConfig[K]): void {
-    // Don't bother setting the option if it is already the same.
-    const oldValue = getOption(editor, option);
-    if (oldValue === value) {
-      return;
-    }
+    let el = editor.getWrapperElement();
     switch (option) {
     case 'lineWrap':
       editor.setOption('lineWrapping', value);
@@ -1198,10 +1207,18 @@ namespace Private {
       editor.setOption('autoCloseBrackets', value);
       break;
     case 'readOnly':
-      let el = editor.getWrapperElement();
       el.classList.toggle(READ_ONLY_CLASS, value);
       editor.setOption(option, value);
       break;
+    case 'fontFamily':
+      el.style.fontFamily = value;
+      break;
+    case 'fontSize':
+      el.style.fontSize = value ? value + 'px' : null;
+      break;
+    case 'lineHeight':
+      el.style.lineHeight = value ? value.toString() : null;
+      break;
     default:
       editor.setOption(option, value);
       break;

packages/fileeditor-extension/schema/plugin.json

@@ -9,6 +9,17 @@
         "autoClosingBrackets": {
           "type": "boolean"
         },
+        "fontFamily": {
+          "type": ["string", "null"]
+        },
+        "fontSize": {
+          "type": ["integer", "null"],
+          "minimum": 1,
+          "maximum": 100
+        },
+        "lineHeight": {
+          "type": ["number", "null"]
+        },
         "lineNumbers": {
           "type": "boolean"
         },
@@ -35,10 +46,13 @@
   "properties": {
     "editorConfig": {
       "title": "Editor Configuration",
-      "description": "The configuration for all text editors.",
+      "description": "The configuration for all text editors.\nIf `fontFamily`, `fontSize` or `lineHeight` are `null`, values from\ncurrent theme are used.",
       "$ref": "#/definitions/editorConfig",
       "default": {
         "autoClosingBrackets": true,
+        "fontFamily": null,
+        "fontSize": null,
+        "lineHeight": null,
         "lineNumbers": true,
         "lineWrap": true,
         "matchBrackets": true,

packages/notebook-extension/schema/tracker.json

@@ -9,6 +9,17 @@
         "autoClosingBrackets": {
           "type": "boolean"
         },
+        "fontFamily": {
+          "type": ["string", "null"]
+        },
+        "fontSize": {
+          "type": ["integer", "null"],
+          "minimum": 1,
+          "maximum": 100
+        },
+        "lineHeight": {
+          "type": ["number", "null"]
+        },
         "lineNumbers": {
           "type": "boolean"
         },
@@ -39,6 +50,9 @@
       "$ref": "#/definitions/editorConfig",
       "default": {
         "autoClosingBrackets": true,
+        "fontFamily": null,
+        "fontSize": null,
+        "lineHeight": null,
         "lineNumbers": false,
         "lineWrap": false,
         "matchBrackets": true,
@@ -53,6 +67,9 @@
       "$ref": "#/definitions/editorConfig",
       "default": {
         "autoClosingBrackets": false,
+        "fontFamily": null,
+        "fontSize": null,
+        "lineHeight": null,
         "lineNumbers": false,
         "lineWrap": true,
         "matchBrackets": false,
@@ -67,6 +84,9 @@
       "$ref": "#/definitions/editorConfig",
       "default": {
         "autoClosingBrackets": false,
+        "fontFamily": null,
+        "fontSize": null,
+        "lineHeight": null,
         "lineNumbers": false,
         "lineWrap": true,
         "matchBrackets": false,