From 93b6288958bc9627d5bd53e0386ff86ad8f613ac Mon Sep 17 00:00:00 2001 From: Wu Cheng-Han Date: Fri, 25 Sep 2015 19:02:51 +0800 Subject: [PATCH] Updated editor default theme and some other options --- public/js/index.js | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/public/js/index.js b/public/js/index.js index 40e5c5df6..8e1bd41dc 100644 --- a/public/js/index.js +++ b/public/js/index.js @@ -206,10 +206,11 @@ var editor = CodeMirror.fromTextArea(textit, { lineNumbers: true, lineWrapping: true, showCursorWhenSelecting: true, + highlightSelectionMatches: true, indentUnit: 4, indentWithTabs: true, continueComments: "Enter", - theme: "monokai", + theme: "one-dark", inputStyle: "textarea", matchBrackets: true, autoCloseBrackets: true, @@ -220,6 +221,8 @@ var editor = CodeMirror.fromTextArea(textit, { foldGutter: true, gutters: ["CodeMirror-linenumbers", "CodeMirror-foldgutter"], extraKeys: defaultExtraKeys, + flattenSpans: true, + addModeClass: true, readOnly: true }); var inlineAttach = inlineAttachment.editors.codemirror4.attach(editor);