diff --git a/rsconcept/frontend/src/features/rsform/components/rs-input/rs-input.tsx b/rsconcept/frontend/src/features/rsform/components/rs-input/rs-input.tsx index 4756cbcf..7dd72224 100644 --- a/rsconcept/frontend/src/features/rsform/components/rs-input/rs-input.tsx +++ b/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( ...(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): boolean { + const text = new RSTextWrapper(thisRef.current as Required); + 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) { if (!thisRef.current) { return; } - const text = new RSTextWrapper(thisRef.current as Required); - 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(); + if (processInput(event)) { event.preventDefault(); event.stopPropagation(); } diff --git a/rsconcept/frontend/src/features/rsform/components/rs-input/text-editing.ts b/rsconcept/frontend/src/features/rsform/components/rs-input/text-editing.ts index 9667e3f5..33518db0 100644 --- a/rsconcept/frontend/src/features/rsform/components/rs-input/text-editing.ts +++ b/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('≠'); diff --git a/rsconcept/frontend/src/features/rsform/pages/rsform-page/editor-rsexpression/editor-rsexpression.tsx b/rsconcept/frontend/src/features/rsform/pages/rsform-page/editor-rsexpression/editor-rsexpression.tsx index 81deb109..1b47d38b 100644 --- a/rsconcept/frontend/src/features/rsform/pages/rsform-page/editor-rsexpression/editor-rsexpression.tsx +++ b/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); if (id === TokenID.ID_LOCAL) { - text.insertChar(key ?? 'unknown_local'); + text.replaceWith(key ?? 'unknown_local'); } else { text.insertToken(id); } diff --git a/rsconcept/frontend/src/utils/codemirror.ts b/rsconcept/frontend/src/utils/codemirror.ts index be4357cc..54c1234a 100644 --- a/rsconcept/frontend/src/utils/codemirror.ts +++ b/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)); }