F: Replace ligature combinations with unicode symbols

rsconcept/frontend/src/features/rsform/components/rs-input/rs-input.tsx

@@ -23,7 +23,7 @@ import { extractGlobals } from '../../models/rslang-api';
 import { ccBracketMatching } from './bracket-matching';
 import { rsNavigation } from './click-navigation';
 import { RSLanguage } from './rslang';
-import { getSymbolSubstitute, RSTextWrapper } from './text-editing';
+import { getLigatureSymbol, getSymbolSubstitute, isPotentialLigature, RSTextWrapper } from './text-editing';
 import { rsHoverTooltip } from './tooltip';
 
 const editorSetup: BasicSetupOptions = {
@@ -130,56 +130,77 @@ export const RSInput = forwardRef<ReactCodeMirrorRef, RSInputProps>(
       ...(noTooltip || !schema ? [] : [rsHoverTooltip(schema, onOpenEdit !== undefined)])
     ];
 
+    function handleAutoComplete(text: RSTextWrapper): boolean {
+      const selection = text.getSelection();
+      if (!selection.empty || !schema) {
+        return false;
+      }
+      const wordRange = text.getWord(selection.from);
+      if (!wordRange) {
+        return false;
+      }
+      const word = text.getText(wordRange.from, wordRange.to);
+      if (word.length > 2 && (word.startsWith('Pr') || word.startsWith('pr'))) {
+        text.setSelection(wordRange.from, wordRange.from + 2);
+        if (word.startsWith('Pr')) {
+          text.replaceWith('pr');
+        } else {
+          text.replaceWith('Pr');
+        }
+        return true;
+      }
+      const hint = text.getText(selection.from - 1, selection.from);
+      const type = guessCstType(hint);
+      if (hint === getCstTypePrefix(type)) {
+        text.setSelection(selection.from - 1, selection.from);
+      }
+      const takenAliases = [...extractGlobals(thisRef.current?.view?.state.doc.toString() ?? '')];
+      const newAlias = generateAlias(type, schema, takenAliases);
+      text.replaceWith(newAlias);
+      return true;
+    }
+
+    function processInput(event: React.KeyboardEvent<HTMLDivElement>): boolean {
+      const text = new RSTextWrapper(thisRef.current as Required<ReactCodeMirrorRef>);
+      if ((event.ctrlKey || event.metaKey) && event.code === 'Space') {
+        return handleAutoComplete(text);
+      }
+
+      if (event.altKey) {
+        return text.processAltKey(event.code, event.shiftKey);
+      }
+
+      if (!(event.ctrlKey || event.metaKey)) {
+        if (isPotentialLigature(event.key)) {
+          const selection = text.getSelection();
+          const prevSymbol = text.getText(selection.from - 1, selection.from);
+          const newSymbol = getLigatureSymbol(prevSymbol, event.key);
+          if (newSymbol) {
+            text.setSelection(selection.from - 1, selection.to);
+            text.replaceWith(newSymbol);
+          }
+          return !!newSymbol;
+        } else {
+          const newSymbol = getSymbolSubstitute(event.code, event.shiftKey);
+          if (newSymbol) {
+            text.replaceWith(newSymbol);
+          }
+          return !!newSymbol;
+        }
+      }
+
+      if (event.code === 'KeyQ' && onAnalyze) {
+        onAnalyze();
+        return true;
+      }
+      return false;
+    }
+
     function handleInput(event: React.KeyboardEvent<HTMLDivElement>) {
       if (!thisRef.current) {
         return;
       }
-      const text = new RSTextWrapper(thisRef.current as Required<ReactCodeMirrorRef>);
+      if (processInput(event)) {
-      if ((event.ctrlKey || event.metaKey) && event.code === 'Space') {
-        const selection = text.getSelection();
-        if (!selection.empty || !schema) {
-          return;
-        }
-        const wordRange = text.getWord(selection.from);
-        if (wordRange) {
-          const word = text.getText(wordRange.from, wordRange.to);
-          if (word.length > 2 && (word.startsWith('Pr') || word.startsWith('pr'))) {
-            text.setSelection(wordRange.from, wordRange.from + 2);
-            if (word.startsWith('Pr')) {
-              text.replaceWith('pr');
-            } else {
-              text.replaceWith('Pr');
-            }
-            event.preventDefault();
-            event.stopPropagation();
-            return;
-          }
-        }
-
-        const hint = text.getText(selection.from - 1, selection.from);
-        const type = guessCstType(hint);
-        if (hint === getCstTypePrefix(type)) {
-          text.setSelection(selection.from - 1, selection.from);
-        }
-        const takenAliases = [...extractGlobals(thisRef.current.view?.state.doc.toString() ?? '')];
-        const newAlias = generateAlias(type, schema, takenAliases);
-        text.replaceWith(newAlias);
-        event.preventDefault();
-        event.stopPropagation();
-      } else if (event.altKey) {
-        if (text.processAltKey(event.code, event.shiftKey)) {
-          event.preventDefault();
-          event.stopPropagation();
-        }
-      } else if (!(event.ctrlKey || event.metaKey)) {
-        const newSymbol = getSymbolSubstitute(event.code, event.shiftKey);
-        if (newSymbol) {
-          text.replaceWith(newSymbol);
-          event.preventDefault();
-          event.stopPropagation();
-        }
-      } else if (event.code === 'KeyQ' && onAnalyze) {
-        onAnalyze();
         event.preventDefault();
         event.stopPropagation();
       }

rsconcept/frontend/src/features/rsform/components/rs-input/text-editing.ts

@@ -6,6 +6,24 @@ import { CodeMirrorWrapper } from '@/utils/codemirror';
 
 import { TokenID } from '../../backend/types';
 
+/* Determines whether an input key is a potential ligature. */
+export function isPotentialLigature(text: string): boolean {
+  return text == '=';
+}
+
+/* Determines symbol for ligature replacement. */
+export function getLigatureSymbol(prevSymbol: string, text: string): string | undefined {
+  if (text == '=') {
+    // prettier-ignore
+    switch (prevSymbol) {
+    case '!': return '≠';
+    case '>': return '≥';
+    case '<': return '≤';
+  }
+  }
+  return undefined;
+}
+
 export function getSymbolSubstitute(keyCode: string, shiftPressed: boolean): string | undefined {
   // prettier-ignore
   if (shiftPressed) {
@@ -172,7 +190,12 @@ export class RSTextWrapper extends CodeMirrorWrapper {
         this.replaceWith('∃');
         return true;
       case TokenID.SET_IN:
-        this.replaceWith('∈');
+        if (this.getPrevSymbol() == '!') {
+          this.setSelection(selection.from - 1, selection.to);
+          this.replaceWith('∉');
+        } else {
+          this.replaceWith('∈');
+        }
         return true;
       case TokenID.SET_NOT_IN:
         this.replaceWith('∉');
@@ -184,7 +207,12 @@ export class RSTextWrapper extends CodeMirrorWrapper {
         this.replaceWith('&');
         return true;
       case TokenID.SUBSET_OR_EQ:
-        this.replaceWith('⊆');
+        if (this.getPrevSymbol() == '!') {
+          this.setSelection(selection.from - 1, selection.to);
+          this.replaceWith('⊄');
+        } else {
+          this.replaceWith('⊆');
+        }
         return true;
       case TokenID.LOGIC_IMPLICATION:
         this.replaceWith('⇒');
@@ -208,13 +236,23 @@ export class RSTextWrapper extends CodeMirrorWrapper {
         this.replaceWith('Z');
         return true;
       case TokenID.SUBSET:
-        this.replaceWith('⊂');
+        if (this.getPrevSymbol() == '!') {
+          this.setSelection(selection.from - 1, selection.to);
+          this.replaceWith('⊄');
+        } else {
+          this.replaceWith('⊂');
+        }
         return true;
       case TokenID.NOT_SUBSET:
         this.replaceWith('⊄');
         return true;
       case TokenID.EQUAL:
-        this.replaceWith('=');
+        if (this.getPrevSymbol() == '!') {
+          this.setSelection(selection.from - 1, selection.to);
+          this.replaceWith('≠');
+        } else {
+          this.replaceWith('=');
+        }
         return true;
       case TokenID.NOTEQUAL:
         this.replaceWith('≠');

rsconcept/frontend/src/features/rsform/pages/rsform-page/editor-rsexpression/editor-rsexpression.tsx

@@ -133,7 +133,7 @@ export function EditorRSExpression({
     }
     const text = new RSTextWrapper(rsInput.current as Required<ReactCodeMirrorRef>);
     if (id === TokenID.ID_LOCAL) {
-      text.insertChar(key ?? 'unknown_local');
+      text.replaceWith(key ?? 'unknown_local');
     } else {
       text.insertToken(id);
     }

rsconcept/frontend/src/utils/codemirror.ts

@@ -123,6 +123,11 @@ export class CodeMirrorWrapper {
     this.ref = object;
   }
 
+  getPrevSymbol(): string {
+    const selection = this.getSelection();
+    return this.getText(selection.from - 1, selection.from);
+  }
+
   getText(from: number, to: number): string {
     return this.ref.view.state.doc.sliceString(from, to);
   }
@@ -149,10 +154,6 @@ export class CodeMirrorWrapper {
     });
   }
 
-  insertChar(key: string) {
-    this.replaceWith(key);
-  }
-
   replaceWith(data: string) {
     this.ref.view.dispatch(this.ref.view.state.replaceSelection(data));
   }