Merge pull request #1460 from blink1073/remove-extra-codeeditor

Remove the `extra` parameter from `CodeEditor.IOptions`

src/codeeditor/editor.ts

@@ -672,10 +672,5 @@ namespace CodeEditor {
      * The default selection style for the editor.
      */
     selectionStyle?: CodeEditor.ISelectionStyle;
-
-    /**
-     * Extra options.
-     */
-    extra?: { [key: string]: any };
   }
 }

src/codemirror/editor.ts

@@ -83,14 +83,6 @@ class CodeMirrorEditor implements CodeEditor.IEditor {
     let editor = this._editor = CodeMirror(options.host, config);
     let doc = editor.getDoc();
 
-    // Handle extra config.
-    const extra = options.extra;
-    if (extra) {
-      for (const option in extra) {
-        editor.setOption(option, extra[option]);
-      }
-    }
-
     // Handle initial values for text, mimetype, and selections.
     doc.setValue(model.value.text);
     this._onMimeTypeChanged();