From 2dfaa22c35f5872976d64876bab66b073e8ac0f1 Mon Sep 17 00:00:00 2001
From: tophf <tophf@gmx.com>
Date: Thu, 21 Dec 2017 02:29:24 +0300
Subject: [PATCH] Ctrl-Pause defocuses/focuses the editor

---
 edit/codemirror-default.js | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

diff --git a/edit/codemirror-default.js b/edit/codemirror-default.js
index 51325327..d664d77c 100644
--- a/edit/codemirror-default.js
+++ b/edit/codemirror-default.js
@@ -1,4 +1,4 @@
-/* global CodeMirror prefs loadScript editor */
+/* global CodeMirror prefs loadScript editor editors */
 
 'use strict';
 
@@ -27,7 +27,6 @@
     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'
@@ -41,6 +40,19 @@
     cm.blockComment(cm.getCursor('from'), cm.getCursor('to'), {fullLines: false});
   };
 
+  // Ctrl-Pause defocuses/focuses the editor
+  addEventListener('keydown', event => {
+    if (event.code === 'Pause' && event.ctrlKey && !event.shiftKey && !event.altKey && !event.metaKey) {
+      event.preventDefault();
+      const cm = window.editors && (editors.lastActive || editors[0]) || ($('.CodeMirror') || {}).CodeMirror;
+      if (cm && cm.hasFocus()) {
+        setTimeout(() => cm.display.input.blur());
+      } else if (cm) {
+        cm.focus();
+      }
+    }
+  }, true);
+
   // 'basic' keymap only has basic keys by design, so we skip it
 
   const extraKeysCommands = {};