defocus codemirror on Esc

edit/codemirror-default.js

@@ -27,6 +27,7 @@
     keyMap: prefs.get('editor.keyMap'),
     extraKeys: Object.assign(CodeMirror.defaults.extraKeys || {}, {
       // independent of current keyMap
+      'Esc': 'defocusEditor',
       'Alt-Enter': 'toggleStyle',
       'Alt-PageDown': 'nextEditor',
       'Alt-PageUp': 'prevEditor'

edit/codemirror-editing-hooks.js

@@ -13,6 +13,7 @@ onDOMscriptReady('/codemirror.js').then(() => {
     save,
     toggleStyle,
     jumpToLine,
+    defocusEditor,
     nextEditor, prevEditor,
     find, findNext, findPrev, replace, replaceAll,
   };
@@ -155,6 +156,10 @@ onDOMscriptReady('/codemirror.js').then(() => {
     return this.display.wrapper.parentNode;
   }
 
+  function defocusEditor(cm) {
+    cm.display.input.blur();
+  }
+
   function nextEditor(cm) {
     return nextPrevEditor(cm, 1);
   }