From 05dbcff7c3892c21f531b39f81a0c77059dee4e3 Mon Sep 17 00:00:00 2001
From: tophf <tophf@gmx.com>
Date: Tue, 1 May 2018 23:05:13 +0300
Subject: [PATCH] insert spaces on <Tab> when editor.indentWithTabs is false

---
 edit/codemirror-editing-hooks.js | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/edit/codemirror-editing-hooks.js b/edit/codemirror-editing-hooks.js
index 3a8d436f..ac04b275 100644
--- a/edit/codemirror-editing-hooks.js
+++ b/edit/codemirror-editing-hooks.js
@@ -19,6 +19,9 @@ onDOMscriptReady('/codemirror.js').then(() => {
     nextEditor, prevEditor,
     commentSelection,
   };
+  const ORIGINAL_COMMANDS = {
+    insertTab: CodeMirror.commands.insertTab,
+  };
   // reroute handling to nearest editor when keypress resolves to one of these commands
   const REROUTED = new Set([
     'save',
@@ -244,6 +247,12 @@ onDOMscriptReady('/codemirror.js').then(() => {
         CodeMirror.setOption('indentUnit', value);
         break;
 
+      case 'indentWithTabs':
+        CodeMirror.commands.insertTab = value ?
+          ORIGINAL_COMMANDS.insertTab :
+          CodeMirror.commands.insertSoftTab;
+        break;
+
       case 'theme': {
         const themeLink = $('#cm-theme');
         // use non-localized 'default' internally