Make tab usable for alignment

MiniZinc · Oct 6, 2024 · 92557ea · 92557ea
1 parent 4336aa0
commit 92557ea
Show file tree

Hide file tree

Showing 3 changed files with 110 additions and 86 deletions.
diff --git a/package-lock.json b/package-lock.json
diff --git a/package.json b/package.json
@@ -27,6 +27,7 @@
         "vite": "^5.4.8"
     },
     "dependencies": {
+        "@codemirror/commands": "^6.6.2",
         "@codemirror/lang-html": "^6.4.9",
         "@codemirror/lang-json": "^6.0.1",
         "@fortawesome/fontawesome-svg-core": "^6.6.0",

diff --git a/src/lang/index.js b/src/lang/index.js
@@ -1,8 +1,8 @@
 import { parser } from './minizinc.grammar';
 import { basicSetup } from 'codemirror';
-import { Compartment, EditorState } from '@codemirror/state';
+import { Compartment } from '@codemirror/state';
 import { EditorView, keymap } from '@codemirror/view';
-import { indentWithTab } from '@codemirror/commands';
+import { indentLess, indentMore } from '@codemirror/commands';
 import { createTheme } from 'thememirror';
 import {
     LRLanguage,
@@ -168,7 +168,29 @@ export const darkThemeEffect = theme.reconfigure(darkTheme);
 export function getExtensions(suffix, codeCheck, darkMode, readOnly = false) {
     const extensions = [
         basicSetup,
-        keymap.of([indentWithTab]),
+        keymap.of([
+            {
+                key: 'Tab',
+                preventDefault: true,
+                run: ({ state, dispatch }) => {
+                    if (state.selection.ranges.some((r) => !r.empty)) {
+                        return indentMore({ state, dispatch });
+                    }
+                    dispatch(
+                        state.update(state.replaceSelection('  '), {
+                            scrollIntoView: true,
+                            userEvent: 'input',
+                        }),
+                    );
+                    return true;
+                },
+            },
+            {
+                key: 'Shift-Tab',
+                preventDefault: true,
+                run: indentLess,
+            },
+        ]),
         theme.of(darkMode ? darkTheme : lightTheme),
         EditorView.theme({
             '&': { height: '100%' },