From 8861ec537814c6dded22d607f8fcda96d310b425 Mon Sep 17 00:00:00 2001
From: IRBorisov <8611739+IRBorisov@users.noreply.github.com>
Date: Sat, 22 Jul 2023 03:18:48 +0300
Subject: [PATCH] Improve Consistuenta editing experience

---
 .../src/components/Common/SubmitButton.tsx    |   8 +-
 rsconcept/frontend/src/components/Icons.tsx   |   8 +
 .../pages/RSFormPage/ConstituentEditor.tsx    |  64 ++++--
 .../pages/RSFormPage/ConstituentsSideList.tsx |  42 +++-
 .../pages/RSFormPage/ConstituentsTable.tsx    |   2 +-
 .../src/pages/RSFormPage/ExpressionEditor.tsx | 154 +++++++++----
 .../src/pages/RSFormPage/RSFormCard.tsx       |   9 +-
 .../src/pages/RSFormPage/RSLocalButton.tsx    |  25 +++
 .../{RSEditButton.tsx => RSTokenButton.tsx}   |  10 +-
 .../src/pages/RSFormPage/TablistTools.tsx     |   4 +-
 .../src/pages/RSFormPage/textEditing.ts       | 212 ++++++++++++++++++
 rsconcept/frontend/src/utils/staticUI.ts      |  54 ++---
 rsconcept/frontend/src/utils/textEditing.ts   | 118 ----------
 13 files changed, 473 insertions(+), 237 deletions(-)
 create mode 100644 rsconcept/frontend/src/pages/RSFormPage/RSLocalButton.tsx
 rename rsconcept/frontend/src/pages/RSFormPage/{RSEditButton.tsx => RSTokenButton.tsx} (75%)
 create mode 100644 rsconcept/frontend/src/pages/RSFormPage/textEditing.ts
 delete mode 100644 rsconcept/frontend/src/utils/textEditing.ts

diff --git a/rsconcept/frontend/src/components/Common/SubmitButton.tsx b/rsconcept/frontend/src/components/Common/SubmitButton.tsx
index 7bd1a150..689b2cf3 100644
--- a/rsconcept/frontend/src/components/Common/SubmitButton.tsx
+++ b/rsconcept/frontend/src/components/Common/SubmitButton.tsx
@@ -2,15 +2,17 @@ interface SubmitButtonProps {
   text: string
   loading?: boolean
   disabled?: boolean
+  icon?: React.ReactNode
 }
 
-function SubmitButton({text='ОК', disabled, loading=false}: SubmitButtonProps) {
+function SubmitButton({text='ОК', icon, disabled, loading=false}: SubmitButtonProps) {
   return (
     <button type='submit'
-      className={`px-4 py-2 font-bold disabled:cursor-not-allowed rounded clr-btn-primary ${loading ? ' cursor-progress': ''}`}
+      className={`px-4 py-2 inline-flex items-center gap-2 align-middle justify-center font-bold disabled:cursor-not-allowed rounded clr-btn-primary ${loading ? ' cursor-progress': ''}`}
       disabled={disabled}
     >
-      {text}
+      {icon && <span>{icon}</span>}
+      {text && <span>{text}</span>}
     </button>
   )
 }
diff --git a/rsconcept/frontend/src/components/Icons.tsx b/rsconcept/frontend/src/components/Icons.tsx
index 3cb0068e..70efa8bf 100644
--- a/rsconcept/frontend/src/components/Icons.tsx
+++ b/rsconcept/frontend/src/components/Icons.tsx
@@ -274,4 +274,12 @@ export function ArrowsRotateIcon(props: IconProps) {
       <path d='M12 6v3l4-4-4-4v3a8 8 0 00-8 8c0 1.57.46 3.03 1.24 4.26L6.7 14.8A5.9 5.9 0 016 12a6 6 0 016-6m6.76 1.74L17.3 9.2c.44.84.7 1.8.7 2.8a6 6 0 01-6 6v-3l-4 4 4 4v-3a8 8 0 008-8c0-1.57-.46-3.03-1.24-4.26z' />
     </IconSVG>
   );
+}
+
+export function SaveIcon(props: IconProps) {
+  return (
+    <IconSVG viewbox='0 0 24 24' {...props}> 
+      <path d='M19.35 10.04A7.49 7.49 0 0012 4C9.11 4 6.6 5.64 5.35 8.04A5.994 5.994 0 000 14a6 6 0 006 6h13a5 5 0 005-5c0-2.64-2.05-4.78-4.65-4.96M19 18H6a4 4 0 01-4-4c0-2.05 1.53-3.76 3.56-3.97l1.07-.11.5-.95A5.469 5.469 0 0112 6c2.62 0 4.88 1.86 5.39 4.43l.3 1.5 1.53.11A2.98 2.98 0 0122 15a3 3 0 01-3 3M8 13h2.55v3h2.9v-3H16l-4-4-4 4z' />
+    </IconSVG>
+  );
 }
\ No newline at end of file
diff --git a/rsconcept/frontend/src/pages/RSFormPage/ConstituentEditor.tsx b/rsconcept/frontend/src/pages/RSFormPage/ConstituentEditor.tsx
index 30b6f190..d8ee6b2a 100644
--- a/rsconcept/frontend/src/pages/RSFormPage/ConstituentEditor.tsx
+++ b/rsconcept/frontend/src/pages/RSFormPage/ConstituentEditor.tsx
@@ -7,6 +7,7 @@ import ExpressionEditor from './ExpressionEditor';
 import SubmitButton from '../../components/Common/SubmitButton';
 import { getCstTypeLabel } from '../../utils/staticUI';
 import ConstituentsSideList from './ConstituentsSideList';
+import { SaveIcon } from '../../components/Icons';
 
 function ConstituentEditor() {
   const { 
@@ -78,27 +79,38 @@ function ConstituentEditor() {
   return (
     <div className='flex items-start w-full gap-2'>
       <form onSubmit={handleSubmit} className='flex-grow min-w-[50rem] max-w-min px-4 py-2 border'>
-        <div className='flex items-start justify-between gap-1'>
-          <span className='mr-12'>
-            <label 
-              title='Переименовать конституенту' 
-              className='font-semibold underline cursor-pointer'
-              onClick={handleRename}
-            >
-              ID
-            </label>
-            <b className='ml-2'>{alias}</b>
-          </span>
-          <span>
-            <label 
-              title='Изменить тип конституенты'
-              className='font-semibold underline cursor-pointer'
-              onClick={handleChangeType}
-            >
-              Тип
-            </label>
-            <span className='ml-2'>{type}</span>
-          </span>
+        <div className='flex items-start justify-between'>
+          <div className='flex items-start justify-center w-full gap-4'>
+            <span className='mr-12'>
+              <label 
+                title='Переименовать конституенту' 
+                className='font-semibold underline cursor-pointer'
+                onClick={handleRename}
+              >
+                ID
+              </label>
+              <b className='ml-2'>{alias}</b>
+            </span>
+            <span>
+              <label 
+                title='Изменить тип конституенты'
+                className='font-semibold underline cursor-pointer'
+                onClick={handleChangeType}
+              >
+                Тип
+              </label>
+              <span className='ml-2'>{type}</span>
+            </span>
+          </div>
+          <div className='flex justify-end'>
+          <button type='submit'
+            title='Сохранить изменения'
+            className={'px-1 py-1 whitespace-nowrap font-bold disabled:cursor-not-allowed rounded clr-btn-primary'}
+            disabled={!isEditable}
+          >
+            <SaveIcon size={5} />
+          </button>
+          </div>
         </div>
         <TextArea id='term' label='Термин'
           placeholder='Схемный или предметный термин, обозначающий данное понятие или утверждение'
@@ -134,7 +146,7 @@ function ConstituentEditor() {
           onFocus={() => setEditMode(EditMode.TEXT)}
         />
         <TextArea id='convention' label='Конвенция / Комментарий'
-          placeholder='Договоренность об интерпретации неопределяемых понятий или комментарий к производному понятию'
+          placeholder='Договоренность об интерпретации неопределяемого понятия&#x000D;&#x000A;Комментарий к производному понятию'
           rows={4}
           value={convention}
           disabled={!isEditable}
@@ -142,8 +154,12 @@ function ConstituentEditor() {
           onChange={event => setConvention(event.target.value)}
           onFocus={() => setEditMode(EditMode.TEXT)}
         />
-        <div className='mt-2 w-full flex justify-center'>
-          <SubmitButton text='Сохранить изменения' disabled={!isEditable} />
+        <div className='flex justify-center w-full mt-2'>
+          <SubmitButton
+            text='Сохранить изменения'
+            disabled={!isEditable}
+            icon={<SaveIcon size={6} />}
+          />
         </div>
       </form>
       <ConstituentsSideList expression={expression}/>
diff --git a/rsconcept/frontend/src/pages/RSFormPage/ConstituentsSideList.tsx b/rsconcept/frontend/src/pages/RSFormPage/ConstituentsSideList.tsx
index 85a6901e..9d01953c 100644
--- a/rsconcept/frontend/src/pages/RSFormPage/ConstituentsSideList.tsx
+++ b/rsconcept/frontend/src/pages/RSFormPage/ConstituentsSideList.tsx
@@ -1,6 +1,6 @@
 import { useCallback, useState, useMemo, useEffect } from 'react';
 import { useRSForm } from '../../context/RSFormContext';
-import { IConstituenta, matchConstituenta } from '../../utils/models';
+import { CstType, IConstituenta, matchConstituenta } from '../../utils/models';
 import Checkbox from '../../components/Common/Checkbox';
 import DataTableThemed from '../../components/Common/DataTableThemed';
 import useLocalStorage from '../../hooks/useLocalStorage';
@@ -20,8 +20,20 @@ function ConstituentsSideList({expression}: ConstituentsSideListProps) {
     if (!schema?.items) {
       setFilteredData([]);
     } else if (onlyExpression) {
-      const aliases: string[] = extractGlobals(expression);
-      setFilteredData(schema?.items.filter((cst) => aliases.includes(cst.alias)));
+      const aliases = extractGlobals(expression);
+      let filtered = schema?.items.filter((cst) => aliases.has(cst.alias));
+      const names = filtered.map(cst => cst.alias)
+      const diff =  Array.from(aliases).filter(name => names.indexOf(name) < 0);
+      if (diff.length > 0) {
+        diff.forEach(
+          (alias, i) => filtered.push({
+          entityUID: -i,
+          alias: alias,
+          convention: 'Конституента отсутствует',
+          cstType: CstType.BASE
+        }));
+      }
+      setFilteredData(filtered);
     } else if (!filterText) {
       setFilteredData(schema?.items);
     } else {
@@ -31,14 +43,14 @@ function ConstituentsSideList({expression}: ConstituentsSideListProps) {
 
   const handleRowClicked = useCallback(
     (cst: IConstituenta, event: React.MouseEvent<Element, MouseEvent>) => {
-		if (event.ctrlKey) {
+		if (event.altKey && cst.entityUID > 0) {
       setActive(cst);
     }
 	}, [setActive]);
 
   const handleDoubleClick = useCallback(
     (cst: IConstituenta, event: React.MouseEvent<Element, MouseEvent>) => {
-		setActive(cst);
+		if (cst.entityUID > 0) setActive(cst);
 	}, [setActive]);
 
   const columns = useMemo(() => 
@@ -54,13 +66,25 @@ function ConstituentsSideList({expression}: ConstituentsSideListProps) {
         selector: (cst: IConstituenta) => cst.alias,
         width: '62px',
         maxWidth: '62px',
+        conditionalCellStyles: [
+          {
+            when: (cst: IConstituenta) => cst.entityUID <= 0,
+            classNames: ['bg-[#ffc9c9]', 'dark:bg-[#592b2b]']
+          },
+        ],
       },
       {
         name: 'Описание',
         id: 'description',
-        selector: (cst: IConstituenta) => cst.term?.resolved || cst.definition?.text.resolved || cst.definition?.formal || '',
+        selector: (cst: IConstituenta) => cst.term?.resolved || cst.definition?.text.resolved || cst.definition?.formal || cst.convention || '',
         minWidth: '350px',
         wrap: true,
+        conditionalCellStyles: [
+          {
+            when: (cst: IConstituenta) => cst.entityUID <= 0,
+            classNames: ['bg-[#ffc9c9]', 'dark:bg-[#592b2b]']
+          },
+        ],
       },
       {
         name: 'Выражение',
@@ -70,6 +94,12 @@ function ConstituentsSideList({expression}: ConstituentsSideListProps) {
         hide: 1600,
         grow: 2,
         wrap: true,
+        conditionalCellStyles: [
+          {
+            when: (cst: IConstituenta) => cst.entityUID <= 0,
+            classNames: ['bg-[#ffc9c9]', 'dark:bg-[#592b2b]']
+          },
+        ],
       }
     ], []
   );
diff --git a/rsconcept/frontend/src/pages/RSFormPage/ConstituentsTable.tsx b/rsconcept/frontend/src/pages/RSFormPage/ConstituentsTable.tsx
index 2662d72e..dcc486f5 100644
--- a/rsconcept/frontend/src/pages/RSFormPage/ConstituentsTable.tsx
+++ b/rsconcept/frontend/src/pages/RSFormPage/ConstituentsTable.tsx
@@ -24,7 +24,7 @@ function ConstituentsTable({onOpenEdit}: ConstituentsTableProps) {
 
   const handleRowClicked = useCallback(
     (cst: IConstituenta, event: React.MouseEvent<Element, MouseEvent>) => {
-		if (event.ctrlKey) {
+		if (event.altKey) {
       onOpenEdit(cst);
     }
 	}, [onOpenEdit]);
diff --git a/rsconcept/frontend/src/pages/RSFormPage/ExpressionEditor.tsx b/rsconcept/frontend/src/pages/RSFormPage/ExpressionEditor.tsx
index 235db6df..be078053 100644
--- a/rsconcept/frontend/src/pages/RSFormPage/ExpressionEditor.tsx
+++ b/rsconcept/frontend/src/pages/RSFormPage/ExpressionEditor.tsx
@@ -3,14 +3,15 @@ import Button from '../../components/Common/Button';
 import Label from '../../components/Common/Label';
 import { useRSForm } from '../../context/RSFormContext';
 import { toast } from 'react-toastify';
-import RSEditButton from './RSEditButton';
+import RSTokenButton from './RSTokenButton';
 import { CstType, TokenID } from '../../utils/models';
 import useCheckExpression from '../../hooks/useCheckExpression';
 import ParsingResult from './ParsingResult';
 import { Loader } from '../../components/Common/Loader';
 import StatusBar from './StatusBar';
 import { AxiosResponse } from 'axios';
-import { TextWrapper } from '../../utils/textEditing';
+import { TextWrapper, getSymbolSubstitute } from './textEditing';
+import RSLocalButton from './RSLocalButton';
 
 interface ExpressionEditorProps {
   id: string
@@ -50,16 +51,21 @@ function ExpressionEditor({
     });
   }, [value, checkExpression, active, setTypification]);
 
-  const handleEdit = useCallback((id: TokenID) => {
+  const handleEdit = useCallback((id: TokenID, key?: string) => {
     if (!expressionCtrl.current) {
       toast.error('Нет доступа к полю редактирования формального выражения');
       return;
     }
     let text = new TextWrapper(expressionCtrl.current);
-    text.insertToken(id);
+    if (id === TokenID.ID_LOCAL) {
+      text.insertChar(key!);
+    } else {
+      text.insertToken(id);
+    }
     text.finalize();
     text.focus();
     setValue(text.value);
+    setIsModified(true);
   }, [setValue]);
 
   const handleChange = useCallback((event: React.ChangeEvent<HTMLTextAreaElement>) => {
@@ -67,57 +73,106 @@ function ExpressionEditor({
     setIsModified(true);
   }, [setIsModified, onChange]);
 
+  const handleInput = useCallback((event: React.KeyboardEvent<HTMLTextAreaElement>) => {
+    if (event.altKey) {
+      let text = new TextWrapper(expressionCtrl.current!);
+      if (text.processAltKey(event.key)) {
+        event.preventDefault();
+        text.finalize();
+        setValue(text.value);
+        setIsModified(true);
+      }
+    } else if (!event.ctrlKey) {
+      const newSymbol = getSymbolSubstitute(event.key);
+      if (newSymbol) {
+        event.preventDefault();
+        let text = new TextWrapper(expressionCtrl.current!);
+        text.replaceWith(newSymbol);
+        text.finalize();
+        setValue(text.value);
+        setIsModified(true);
+      }
+    }
+  }, [expressionCtrl, setValue]);
 
   const handleFocusIn = useCallback(() => {
     toggleEditMode()
   }, [toggleEditMode]);
 
   const EditButtons = useMemo( () => {
-    return (<div className='w-full text-sm'>
-    <div className='flex justify-start'>
-      <RSEditButton id={TokenID.NT_DECLARATIVE_EXPR} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.NT_IMPERATIVE_EXPR} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.NT_RECURSIVE_FULL} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.BIGPR} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.SMALLPR} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.FILTER} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.REDUCE} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.CARD} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.BOOL} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.DEBOOL} onInsert={handleEdit}/>
+    return (<div className='flex items-center justify-between w-full'>
+    <div className='text-sm w-fit'>
+      <div className='flex justify-start'>
+        <RSTokenButton id={TokenID.NT_DECLARATIVE_EXPR} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.NT_IMPERATIVE_EXPR} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.NT_RECURSIVE_FULL} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.BIGPR} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.SMALLPR} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.FILTER} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.REDUCE} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.CARD} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.BOOL} onInsert={handleEdit}/>
+        
+      </div>
+      <div className='flex justify-start'>
+        <RSTokenButton id={TokenID.BOOLEAN} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.PUNC_PL} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.INTERSECTION} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.LIT_EMPTYSET} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.FORALL} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.NOT} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.IN} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.SUBSET_OR_EQ} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.AND} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.IMPLICATION} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.SET_MINUS} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.PUNC_ITERATE} onInsert={handleEdit}/>      
+        <RSTokenButton id={TokenID.SUBSET} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.DEBOOL} onInsert={handleEdit}/>
+      </div>
+      <div className='flex justify-start'>
+        <RSTokenButton id={TokenID.DECART} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.PUNC_SL} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.UNION} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.LIT_INTSET} onInsert={handleEdit}/>  
+        <RSTokenButton id={TokenID.EXISTS} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.NOTEQUAL} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.NOTIN} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.NOTSUBSET} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.OR} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.EQUIVALENT} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.SYMMINUS} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.PUNC_ASSIGN} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.EQUAL} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.GREATER_OR_EQ} onInsert={handleEdit}/>
+        <RSTokenButton id={TokenID.LESSER_OR_EQ} onInsert={handleEdit}/>
+      </div>
     </div>
-    <div className='flex justify-start'>
-      <RSEditButton id={TokenID.BOOLEAN} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.PUNC_PL} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.FORALL} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.IN} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.OR} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.SUBSET_OR_EQ} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.INTERSECTION} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.MINUS} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.LIT_EMPTYSET} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.SUBSET} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.EQUAL} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.NOT} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.GREATER_OR_EQ} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.LESSER_OR_EQ} onInsert={handleEdit}/>
-      
-    </div>
-    <div className='flex justify-start'>
-      <RSEditButton id={TokenID.DECART} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.PUNC_SL} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.EXISTS} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.NOTIN} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.AND} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.IMPLICATION} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.UNION} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.SYMMINUS} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.LIT_INTSET} onInsert={handleEdit}/>      
-      <RSEditButton id={TokenID.NOTSUBSET} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.NOTEQUAL} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.EQUIVALENT} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.PUNC_ASSIGN} onInsert={handleEdit}/>
-      <RSEditButton id={TokenID.PUNC_ITERATE} onInsert={handleEdit}/>
+    <div className='text-xs w-fit'>
+      <div className='flex justify-start'>
+        <RSLocalButton text='μ' tooltip='q' onInsert={handleEdit}/>
+        <RSLocalButton text='ω' tooltip='w' onInsert={handleEdit}/>
+        <RSLocalButton text='ε' tooltip='e' onInsert={handleEdit}/>
+        <RSLocalButton text='ρ' tooltip='r' onInsert={handleEdit}/>
+        <RSLocalButton text='τ' tooltip='t' onInsert={handleEdit}/>
+        <RSLocalButton text='π' tooltip='y' onInsert={handleEdit}/>
+      </div>
+      <div className='flex justify-start'>
+        <RSLocalButton text='α' tooltip='a' onInsert={handleEdit}/>
+        <RSLocalButton text='σ' tooltip='s' onInsert={handleEdit}/>
+        <RSLocalButton text='δ' tooltip='d' onInsert={handleEdit}/>
+        <RSLocalButton text='φ' tooltip='f' onInsert={handleEdit}/>
+        <RSLocalButton text='γ' tooltip='g' onInsert={handleEdit}/>
+        <RSLocalButton text='λ' tooltip='h' onInsert={handleEdit}/>
+      </div>
+      <div className='flex justify-start'>
+        <RSLocalButton text='ζ' tooltip='z' onInsert={handleEdit}/>
+        <RSLocalButton text='ξ' tooltip='x' onInsert={handleEdit}/>
+        <RSLocalButton text='ψ' tooltip='c' onInsert={handleEdit}/>
+        <RSLocalButton text='θ' tooltip='v' onInsert={handleEdit}/>
+        <RSLocalButton text='β' tooltip='b' onInsert={handleEdit}/>
+        <RSLocalButton text='η' tooltip='n' onInsert={handleEdit}/>
+      </div>
     </div>
     </div>);
   }, [handleEdit])
@@ -136,9 +191,10 @@ function ExpressionEditor({
           value={value}
           onChange={handleChange}
           onFocus={handleFocusIn}
+          onKeyDown={handleInput}
           disabled={disabled}
       />
-      <div className='flex gap-4 py-1 mt-1 justify-stretch items-stre'>
+      <div className='flex w-full gap-4 py-1 mt-1 justify-stretch'>
         <div className='flex flex-col gap-2'>
           {isActive && <StatusBar
             isModified={isModified}
diff --git a/rsconcept/frontend/src/pages/RSFormPage/RSFormCard.tsx b/rsconcept/frontend/src/pages/RSFormPage/RSFormCard.tsx
index 1e8823db..2e2c40f4 100644
--- a/rsconcept/frontend/src/pages/RSFormPage/RSFormCard.tsx
+++ b/rsconcept/frontend/src/pages/RSFormPage/RSFormCard.tsx
@@ -6,7 +6,7 @@ import TextInput from '../../components/Common/TextInput';
 import { useRSForm } from '../../context/RSFormContext';
 import { useCallback, useEffect, useState } from 'react';
 import Button from '../../components/Common/Button';
-import { CrownIcon, DownloadIcon, DumpBinIcon, ShareIcon } from '../../components/Icons';
+import { CrownIcon, DownloadIcon, DumpBinIcon, SaveIcon, ShareIcon } from '../../components/Icons';
 import { useUsers } from '../../context/UsersContext';
 import { useNavigate } from 'react-router-dom';
 import { toast } from 'react-toastify';
@@ -86,7 +86,12 @@ function RSFormCard() {
       />
       
       <div className='flex items-center justify-between gap-1 py-2 mt-2'>
-        <SubmitButton text='Сохранить изменения' loading={processing} disabled={!isEditable || processing} />
+        <SubmitButton
+          text='Сохранить изменения' 
+          loading={processing}
+          disabled={!isEditable || processing}
+          icon={<SaveIcon size={6} />}
+        />
         <div className='flex justify-end gap-1'>
           <Button 
             tooltip='Поделиться схемой'
diff --git a/rsconcept/frontend/src/pages/RSFormPage/RSLocalButton.tsx b/rsconcept/frontend/src/pages/RSFormPage/RSLocalButton.tsx
new file mode 100644
index 00000000..37d19e10
--- /dev/null
+++ b/rsconcept/frontend/src/pages/RSFormPage/RSLocalButton.tsx
@@ -0,0 +1,25 @@
+import { TokenID } from '../../utils/models'
+
+interface  RSLocalButtonProps {
+  text: string
+  tooltip: string
+  disabled?: boolean
+  onInsert: (token: TokenID, key?: string) => void
+}
+
+function RSLocalButton({text, tooltip, disabled, onInsert}: RSLocalButtonProps) {
+  return (
+    <button
+      type='button'
+      disabled={disabled}
+      onClick={() => onInsert(TokenID.ID_LOCAL, text)}
+      title={tooltip}
+      tabIndex={-1}
+      className='w-[1.5rem] h-7 cursor-pointer border rounded-none clr-btn-clear'
+    >
+      {text}
+    </button>
+  );
+}
+
+export default RSLocalButton;
\ No newline at end of file
diff --git a/rsconcept/frontend/src/pages/RSFormPage/RSEditButton.tsx b/rsconcept/frontend/src/pages/RSFormPage/RSTokenButton.tsx
similarity index 75%
rename from rsconcept/frontend/src/pages/RSFormPage/RSEditButton.tsx
rename to rsconcept/frontend/src/pages/RSFormPage/RSTokenButton.tsx
index d73d8393..c22d48c5 100644
--- a/rsconcept/frontend/src/pages/RSFormPage/RSEditButton.tsx
+++ b/rsconcept/frontend/src/pages/RSFormPage/RSTokenButton.tsx
@@ -1,13 +1,13 @@
 import { TokenID } from '../../utils/models'
 import { getRSButtonData } from '../../utils/staticUI'
 
-interface RSEditButtonProps {
+interface  RSTokenButtonProps {
   id: TokenID
   disabled?: boolean
-  onInsert: (token: TokenID) => void
+  onInsert: (token: TokenID, key?: string) => void
 }
 
-function RSEditButton({id, disabled, onInsert}: RSEditButtonProps) {
+function RSTokenButton({id, disabled, onInsert}: RSTokenButtonProps) {
   const data = getRSButtonData(id);
   const width = data.text.length > 3 ? 'w-[4rem]' : 'w-[2rem]';
   return (
@@ -21,7 +21,7 @@ function RSEditButton({id, disabled, onInsert}: RSEditButtonProps) {
     >
       {data.text && <span className='whitespace-nowrap'>{data.text}</span>}
     </button>
-  )
+  );
 }
 
-export default RSEditButton;
\ No newline at end of file
+export default RSTokenButton;
\ No newline at end of file
diff --git a/rsconcept/frontend/src/pages/RSFormPage/TablistTools.tsx b/rsconcept/frontend/src/pages/RSFormPage/TablistTools.tsx
index f95404bf..a98888ef 100644
--- a/rsconcept/frontend/src/pages/RSFormPage/TablistTools.tsx
+++ b/rsconcept/frontend/src/pages/RSFormPage/TablistTools.tsx
@@ -102,7 +102,7 @@ function TablistTools() {
       </div>
       <div ref={editMenu.ref}>
         <Button
-          tooltip={'измнение ' + (isEditable ? 'доступно': 'запрещено')}
+          tooltip={'измнение: ' + (isEditable ? '[доступно]': '[запрещено]')}
           borderClass=''
           icon={<PenIcon size={5} color={isEditable ? 'text-green': 'text-red'}/>}
           dense
@@ -130,7 +130,7 @@ function TablistTools() {
       </div>
       <div>
         <Button
-          tooltip={'отслеживание: ' + (isTracking ? 'включено': 'выключено')}
+          tooltip={'отслеживание: ' + (isTracking ? '[включено]': '[выключено]')}
           icon={isTracking ? 
             <EyeIcon color='text-primary' size={5}/> 
             : <EyeOffIcon size={5}/>
diff --git a/rsconcept/frontend/src/pages/RSFormPage/textEditing.ts b/rsconcept/frontend/src/pages/RSFormPage/textEditing.ts
new file mode 100644
index 00000000..d8fb794a
--- /dev/null
+++ b/rsconcept/frontend/src/pages/RSFormPage/textEditing.ts
@@ -0,0 +1,212 @@
+// Formatted text editing helpers
+
+import { TokenID } from '../../utils/models'
+
+export function getSymbolSubstitute(input: string): string | undefined {
+  switch(input) {
+  case '`': return '∀';
+  case '~': return '∃';
+
+  // qwerty = μωερτπ
+  //  asdfgh = ασδφγλ
+  //   zxcvbn = ζξψθβη
+  case 'q': return 'μ';
+  case 'w': return 'ω';
+  case 'e': return 'ε';
+  case 'r': return 'ρ';
+  case 't': return 'τ';
+  case 'y': return 'π';
+
+  case 'a': return 'α';
+  case 's': return 'σ';
+  case 'd': return 'δ';
+  case 'f': return 'φ';
+  case 'g': return 'γ';
+  case 'h': return 'λ';
+
+  case 'z': return 'ζ';
+  case 'x': return 'ξ';
+  case 'c': return 'ψ';
+  case 'v': return 'θ';
+  case 'b': return 'β';
+  case 'n': return 'η';
+  }
+  return undefined;
+}
+
+export interface IManagedText {
+  value: string
+  selStart: number
+  selEnd: number
+}
+
+// Note: Wrapper class for textareafield.
+// WARNING! Manipulations on value do not support UNDO browser
+// WARNING! No checks for selection out of text boundaries
+export class TextWrapper implements IManagedText {
+  value: string
+  selStart: number
+  selEnd: number
+  object: HTMLTextAreaElement
+
+  constructor(element: HTMLTextAreaElement) {
+    this.object = element;
+    this.value = this.object.value;
+    this.selStart = this.object.selectionStart;
+    this.selEnd = this.object.selectionEnd;
+  }
+
+  focus() {
+    this.object.focus();
+  }
+
+  refresh() {
+    this.value = this.object.value;
+    this.selStart = this.object.selectionStart;
+    this.selEnd = this.object.selectionEnd;
+  }
+
+  finalize() {
+    this.object.value = this.value;
+    this.object.selectionStart = this.selStart;
+    this.object.selectionEnd = this.selEnd;
+  }
+ 
+  replaceWith(data: string) {
+    this.value = this.value.substring(0, this.selStart) + data + this.value.substring(this.selEnd, this.value.length);
+    this.selEnd += data.length - this.selEnd + this.selStart;
+    this.selStart = this.selEnd;
+  }
+
+  envelopeWith(left: string, right: string) {
+    this.value = this.value.substring(0, this.selStart) + left + 
+                  this.value.substring(this.selStart, this.selEnd) + right + 
+                  this.value.substring(this.selEnd, this.value.length);
+    this.selEnd += left.length + right.length;
+  }
+
+  moveSel(shift: number) {
+    this.selStart += shift;
+    this.selEnd += shift;
+  }
+
+  setSel(start: number, end: number) {
+    this.selStart = start;
+    this.selEnd = end;
+  }
+
+  insertChar(key: string) {
+    this.replaceWith(key);
+  }
+
+  insertToken(tokenID: TokenID): boolean {
+    switch(tokenID) {
+    case TokenID.NT_DECLARATIVE_EXPR:   this.envelopeWith('D{ξ∈X1 | ', '}'); return true;
+    case TokenID.NT_IMPERATIVE_EXPR:    this.envelopeWith('I{(σ, γ) | σ:∈X1; γ:=F1[σ]; ', '}'); return true;
+    case TokenID.NT_RECURSIVE_FULL:     this.envelopeWith('R{ ξ:=D1 | 1=1 | ', '}'); return true;
+    case TokenID.BIGPR:                 this.envelopeWith('Pr1(', ')'); return true;
+    case TokenID.SMALLPR:               this.envelopeWith('pr1(', ')'); return true;
+    case TokenID.FILTER:                this.envelopeWith('Fi1[α](', ')'); return true;
+    case TokenID.REDUCE:                this.envelopeWith('red(', ')'); return true;
+    case TokenID.CARD:                  this.envelopeWith('card(', ')'); return true;
+    case TokenID.BOOL:                  this.envelopeWith('bool(', ')'); return true;
+    case TokenID.DEBOOL:                this.envelopeWith('debool(', ')'); return true;
+    
+    case TokenID.PUNC_PL: {
+      this.envelopeWith('(', ')');
+      this.selEnd = this.selStart + 1;
+      this.selStart = this.selEnd;
+      return true;
+    }
+    case TokenID.PUNC_SL: {
+      this.envelopeWith('[', ']');
+      this.selEnd = this.selStart + 1;
+      this.selStart = this.selEnd;
+      return true;
+    }
+    case TokenID.BOOLEAN: {
+      if (this.selEnd !== this.selStart && this.value.at(this.selStart) === 'ℬ') {
+        this.envelopeWith('ℬ', '');
+      } else {
+        this.envelopeWith('ℬ(', ')');
+      }
+       return true;
+    }
+    
+    case TokenID.DECART:                this.replaceWith('×'); return true;
+    case TokenID.FORALL:                this.replaceWith('∀'); return true;
+    case TokenID.EXISTS:                this.replaceWith('∃'); return true;
+    case TokenID.IN:                    this.replaceWith('∈'); return true;
+    case TokenID.NOTIN:                 this.replaceWith('∉'); return true;
+    case TokenID.OR:                    this.replaceWith('∨'); return true;
+    case TokenID.AND:                   this.replaceWith('&'); return true;
+    case TokenID.SUBSET_OR_EQ:          this.replaceWith('⊆'); return true;
+    case TokenID.IMPLICATION:           this.replaceWith('⇒'); return true;
+    case TokenID.INTERSECTION:          this.replaceWith('∩'); return true;
+    case TokenID.UNION:                 this.replaceWith('∪'); return true;
+    case TokenID.SET_MINUS:             this.replaceWith('\\'); return true;
+    case TokenID.SYMMINUS:              this.replaceWith('∆'); return true;
+    case TokenID.LIT_EMPTYSET:          this.replaceWith('∅'); return true;
+    case TokenID.LIT_INTSET:            this.replaceWith('Z'); return true;
+    case TokenID.SUBSET:                this.replaceWith('⊂'); return true;
+    case TokenID.NOTSUBSET:             this.replaceWith('⊄'); return true;
+    case TokenID.EQUAL:                 this.replaceWith('='); return true;
+    case TokenID.NOTEQUAL:              this.replaceWith('≠'); return true;
+    case TokenID.NOT:                   this.replaceWith('¬'); return true;
+    case TokenID.EQUIVALENT:            this.replaceWith('⇔'); return true;
+    case TokenID.GREATER_OR_EQ:         this.replaceWith('≥'); return true;
+    case TokenID.LESSER_OR_EQ:          this.replaceWith('≤'); return true;
+    case TokenID.PUNC_ASSIGN:           this.replaceWith(':='); return true;
+    case TokenID.PUNC_ITERATE:          this.replaceWith(':∈'); return true;
+    case TokenID.MULTIPLY:              this.replaceWith('*'); return true;
+    }
+    return false;
+  }
+
+  processAltKey(key: string): boolean {
+  switch(key) {
+    // qwert
+    //  asdfg
+    //   zxcvb
+    case 'q': return this.insertToken(TokenID.BIGPR);
+    case 'w': return this.insertToken(TokenID.SMALLPR);
+    case 'e': return this.insertToken(TokenID.BOOLEAN);
+    case 'r': return this.insertToken(TokenID.REDUCE);
+    case 't': return this.insertToken(TokenID.NT_RECURSIVE_FULL);
+    case 'a': return this.insertToken(TokenID.INTERSECTION);
+    case 's': return this.insertToken(TokenID.UNION);
+    case 'd': return this.insertToken(TokenID.NT_DECLARATIVE_EXPR);
+    case 'f': return this.insertToken(TokenID.FILTER);
+    case 'g': return this.insertToken(TokenID.NT_IMPERATIVE_EXPR);
+    case 'z': return this.insertToken(TokenID.LIT_INTSET);
+    case 'x': return this.insertToken(TokenID.LIT_EMPTYSET);
+    case 'c': return this.insertToken(TokenID.CARD);
+    case 'v': return this.insertToken(TokenID.DEBOOL);
+    case 'b': return this.insertToken(TokenID.BOOL);
+    
+    // `123456
+    // ~!@#$%^
+    case '`': return this.insertToken(TokenID.NOT);
+    case '~': return this.insertToken(TokenID.NOTEQUAL);
+    case '1': return this.insertToken(TokenID.IN);
+    case '!': return this.insertToken(TokenID.NOTIN); // Alt + 1
+    case '2': return this.insertToken(TokenID.SUBSET_OR_EQ);
+    case '@': return this.insertToken(TokenID.NOTSUBSET); // Alt + 2
+    case '3': return this.insertToken(TokenID.AND);
+    case '#': return this.insertToken(TokenID.OR); // Alt + 3
+    case '4': return this.insertToken(TokenID.IMPLICATION);
+    case '$': return this.insertToken(TokenID.EQUIVALENT); // Alt + 4
+    case '5': return this.insertToken(TokenID.SET_MINUS);
+    case '%': return this.insertToken(TokenID.SYMMINUS); // Alt + 5
+    case '6': return this.insertToken(TokenID.PUNC_ITERATE);
+    case '^': return this.insertToken(TokenID.PUNC_ASSIGN); // Alt + 6
+    case '7': return this.insertToken(TokenID.SUBSET);
+    case '&': return this.insertToken(TokenID.GREATER_OR_EQ); // Alt + 7
+    case '8': return this.insertToken(TokenID.MULTIPLY);
+    case '*': return this.insertToken(TokenID.LESSER_OR_EQ); // Alt + 8
+    case '(': return this.insertToken(TokenID.PUNC_PL); // Alt + 9
+    case '[': return this.insertToken(TokenID.PUNC_SL);
+    }
+    return false;
+  }
+};
\ No newline at end of file
diff --git a/rsconcept/frontend/src/utils/staticUI.ts b/rsconcept/frontend/src/utils/staticUI.ts
index 7481a965..966f9948 100644
--- a/rsconcept/frontend/src/utils/staticUI.ts
+++ b/rsconcept/frontend/src/utils/staticUI.ts
@@ -24,8 +24,8 @@ export function getTypeLabel(cst: IConstituenta) {
 export function getRSButtonData(id: TokenID): IRSButtonData {
   switch(id) {
   case TokenID.BOOLEAN: return {
-    text: 'ℬ',
-    tooltip: 'Булеан [Shift + B]',
+    text: 'ℬ()',
+    tooltip: 'Булеан [Alt + E]',
   };
   case TokenID.DECART: return {
     text: '×',
@@ -33,11 +33,11 @@ export function getRSButtonData(id: TokenID): IRSButtonData {
   };
   case TokenID.PUNC_PL: return {
     text: '( )',
-    tooltip: 'Скобки вокруг выражения',
+    tooltip: 'Скобки вокруг выражения [ Alt + Shift + 9 ]',
   };
   case TokenID.PUNC_SL: return {
     text: '[ ]',
-    tooltip: 'Скобки вокруг выражения',
+    tooltip: 'Скобки вокруг выражения [ Alt + [ ]',
   };
   case TokenID.FORALL: return {
     text: '∀',
@@ -49,31 +49,31 @@ export function getRSButtonData(id: TokenID): IRSButtonData {
   };
   case TokenID.NOT: return {
     text: '¬',
-    tooltip: 'Отрицание [Alt + Shift + -]',
+    tooltip: 'Отрицание [Alt + `]',
   };
   case TokenID.AND: return {
     text: '&',
-    tooltip: 'Конъюнкция [Shift + 7]',
+    tooltip: 'Конъюнкция [Alt + 3 ~ Shift + 7]',
   };
   case TokenID.OR: return {
     text: '∨',
-    tooltip: 'дизъюнкция [Alt + Shift + 7]',
+    tooltip: 'дизъюнкция [Alt + Shift + 3]',
   };
   case TokenID.IMPLICATION: return {
     text: '⇒',
-    tooltip: 'импликация [Alt + Shift + ]]',
+    tooltip: 'импликация [Alt + 4]',
   };
   case TokenID.EQUIVALENT: return {
     text: '⇔',
-    tooltip: 'эквивалентность [Alt + Shift + []',
+    tooltip: 'эквивалентность [Alt + Shift + 4]',
   };
   case TokenID.LIT_EMPTYSET: return {
     text: '∅',
-    tooltip: 'пустое множество [Alt + Shift + 0]',
+    tooltip: 'пустое множество [Alt + X]',
   };
   case TokenID.LIT_INTSET: return {
     text: 'Z',
-    tooltip: 'целые числа',
+    tooltip: 'целые числа [Alt + Z]',
   };
   case TokenID.EQUAL: return {
     text: '=',
@@ -81,7 +81,7 @@ export function getRSButtonData(id: TokenID): IRSButtonData {
   };
   case TokenID.NOTEQUAL: return {
     text: '≠',
-    tooltip: 'неравенство [Alt + Shift + =]',
+    tooltip: 'неравенство [Alt + Shift + `]',
   };
   case TokenID.GREATER_OR_EQ: return {
     text: '≥',
@@ -93,7 +93,7 @@ export function getRSButtonData(id: TokenID): IRSButtonData {
   };
   case TokenID.IN: return {
     text: '∈',
-    tooltip: 'принадлежит [Alt + \']',
+    tooltip: 'быть элементом (принадлежит) [Alt + \']',
   };
   case TokenID.NOTIN: return {
     text: '∉',
@@ -101,7 +101,7 @@ export function getRSButtonData(id: TokenID): IRSButtonData {
   };
   case TokenID.SUBSET_OR_EQ: return {
     text: '⊆',
-    tooltip: 'быть частью (нестрогое подмножество) [Alt + Shift + L]',
+    tooltip: 'быть частью (нестрогое подмножество) [Alt + 2]',
   };
   case TokenID.SUBSET: return {
     text: '⊂',
@@ -109,7 +109,7 @@ export function getRSButtonData(id: TokenID): IRSButtonData {
   };
   case TokenID.NOTSUBSET: return {
     text: '⊄',
-    tooltip: 'не подмножество [Alt + Shift + ;]',
+    tooltip: 'не подмножество [Alt + Shift + 2]',
   };
   case TokenID.INTERSECTION: return {
     text: '∩',
@@ -119,36 +119,36 @@ export function getRSButtonData(id: TokenID): IRSButtonData {
     text: '∪',
     tooltip: 'объединение [Alt + U]',
   };
-  case TokenID.MINUS: return {
+  case TokenID.SET_MINUS: return {
     text: '\\',
-    tooltip: 'Разность множеств',
+    tooltip: 'Разность множеств [Alt + 5]',
   };
   case TokenID.SYMMINUS: return {
     text: '∆',
-    tooltip: 'Симметрическая разность',
+    tooltip: 'Симметрическая разность [Alt + Shift + 5]',
   };
   case TokenID.NT_DECLARATIVE_EXPR: return {
     text: 'D{}',
-    tooltip: 'Декларативная форма определения терма',
+    tooltip: 'Декларативная форма определения терма [Alt + D]',
   };
   case TokenID.NT_IMPERATIVE_EXPR: return {
     text: 'I{}',
-    tooltip: 'императивная форма определения терма',
+    tooltip: 'императивная форма определения терма [Alt + G]',
   };
   case TokenID.NT_RECURSIVE_FULL: return {
     text: 'R{}',
-    tooltip: 'рекурсивная (цикличная) форма определения терма',
+    tooltip: 'рекурсивная (цикличная) форма определения терма [Alt + T]',
   };
   case TokenID.BIGPR: return {
     text: 'Pr1()',
-    tooltip: 'большая проекция [Alt + W]',
+    tooltip: 'большая проекция [Alt + Q]',
   };
   case TokenID.SMALLPR: return {
     text: 'pr1()',
-    tooltip: 'малая проекция [Alt + Q]',
+    tooltip: 'малая проекция [Alt + W]',
   };
   case TokenID.FILTER: return {
-    text: 'Fi[]()',
+    text: 'Fi1[]()',
     tooltip: 'фильтр [Alt + F]',
   };
   case TokenID.REDUCE: return {
@@ -165,7 +165,7 @@ export function getRSButtonData(id: TokenID): IRSButtonData {
   };
   case TokenID.DEBOOL: return {
     text: 'debool()',
-    tooltip: 'десинглетон [Alt + D]',
+    tooltip: 'десинглетон [Alt + V]',
   };
   case TokenID.PUNC_ASSIGN: return {
     text: ':=',
@@ -248,6 +248,6 @@ export function getStatusInfo(status?: ExpressionStatus): IStatusInfo {
   };
 }
 
-export function extractGlobals(expression: string) {
-  return expression.match(/[XCSADFPT]\d+/g) || [];
+export function extractGlobals(expression: string): Set<string> {
+  return new Set(expression.match(/[XCSADFPT]\d+/g) || []);
 }
\ No newline at end of file
diff --git a/rsconcept/frontend/src/utils/textEditing.ts b/rsconcept/frontend/src/utils/textEditing.ts
deleted file mode 100644
index e8c9df22..00000000
--- a/rsconcept/frontend/src/utils/textEditing.ts
+++ /dev/null
@@ -1,118 +0,0 @@
-// Formatted text editing helpers
-
-import { TokenID } from './models'
-
-export interface IManagedText {
-  value: string
-  selStart: number
-  selEnd: number
-}
-
-// Note: Wrapper class for textareafield.
-// WARNING! Manipulations on value do not support UNDO browser
-// WARNING! No checks for selection out of text boundaries
-export class TextWrapper implements IManagedText {
-  value: string
-  selStart: number
-  selEnd: number
-  object: HTMLTextAreaElement
-
-  constructor(element: HTMLTextAreaElement) {
-    this.object = element;
-    this.value = this.object.value;
-    this.selStart = this.object.selectionStart;
-    this.selEnd = this.object.selectionEnd;
-  }
-
-  focus() {
-    this.object.focus();
-  }
-
-  refresh() {
-    this.value = this.object.value;
-    this.selStart = this.object.selectionStart;
-    this.selEnd = this.object.selectionEnd;
-  }
-
-  finalize() {
-    this.object.value = this.value;
-    this.object.selectionStart = this.selStart;
-    this.object.selectionEnd = this.selEnd;
-  }
- 
-  replaceWith(data: string) {
-    this.value = this.value.substring(0, this.selStart) + data + this.value.substring(this.selEnd, this.value.length);
-    this.selEnd += data.length - this.selEnd + this.selStart;
-    this.selStart = this.selEnd;
-  }
-
-  envelopeWith(left: string, right: string) {
-    this.value = this.value.substring(0, this.selStart) + left + 
-                  this.value.substring(this.selStart, this.selEnd) + right + 
-                  this.value.substring(this.selEnd, this.value.length);
-    this.selEnd += left.length + right.length;
-  }
-
-  moveSel(shift: number) {
-    this.selStart += shift;
-    this.selEnd += shift;
-  }
-
-  setSel(start: number, end: number) {
-    this.selStart = start;
-    this.selEnd = end;
-  }
-
-  insertToken(tokenID: TokenID) {
-    switch(tokenID) {
-    case TokenID.NT_DECLARATIVE_EXPR: this.envelopeWith('D{ξ∈X1 | ', '}'); return;
-    case TokenID.NT_IMPERATIVE_EXPR: this.envelopeWith('I{(σ, γ) | σ:∈X1; γ:=F1[σ]; ', '}'); return;
-    case TokenID.NT_RECURSIVE_FULL: this.envelopeWith('R{ ξ:=D1 | 1=1 | ', '}'); return;
-    case TokenID.BIGPR: this.envelopeWith('Pr1(', ')'); return;
-    case TokenID.SMALLPR: this.envelopeWith('pr1(', ')'); return;
-    case TokenID.FILTER: this.envelopeWith('Fi1[α](', ')'); return;
-    case TokenID.REDUCE: this.envelopeWith('red(', ')'); return;
-    case TokenID.CARD: this.envelopeWith('card(', ')'); return;
-    case TokenID.BOOL: this.envelopeWith('bool(', ')'); return;
-    case TokenID.DEBOOL: this.envelopeWith('debool(', ')'); return;
-    case TokenID.PUNC_PL: this.envelopeWith('(', ')'); return;
-    case TokenID.PUNC_SL: this.envelopeWith('[', ']'); return;
-
-    case TokenID.BOOLEAN: {
-      if (this.selEnd !== this.selStart && this.value.at(this.selStart) === 'ℬ') {
-        this.envelopeWith('ℬ', '');
-      } else {
-        this.envelopeWith('ℬ(', ')');
-      }
-       return;
-    }
-    
-    case TokenID.DECART: this.replaceWith('×'); return;
-    case TokenID.FORALL: this.replaceWith('∀'); return;
-    case TokenID.EXISTS: this.replaceWith('∃'); return;
-    case TokenID.IN: this.replaceWith('∈'); return;
-    case TokenID.NOTIN: this.replaceWith('∉'); return;
-    case TokenID.OR: this.replaceWith('∨'); return;
-    case TokenID.AND: this.replaceWith('&'); return;
-    case TokenID.SUBSET_OR_EQ: this.replaceWith('⊆'); return;
-    case TokenID.IMPLICATION: this.replaceWith('⇒'); return;
-    case TokenID.INTERSECTION: this.replaceWith('∩'); return;
-    case TokenID.UNION: this.replaceWith('∪'); return;
-    case TokenID.MINUS: this.replaceWith('\\'); return;
-    case TokenID.SYMMINUS: this.replaceWith('∆'); return;
-    case TokenID.LIT_EMPTYSET: this.replaceWith('∅'); return;
-    case TokenID.LIT_INTSET: this.replaceWith('Z'); return;
-    case TokenID.SUBSET: this.replaceWith('⊂'); return;
-    case TokenID.NOTSUBSET: this.replaceWith('⊄'); return;
-    case TokenID.EQUAL: this.replaceWith('='); return;
-    case TokenID.NOTEQUAL: this.replaceWith('≠'); return;
-    case TokenID.NOT: this.replaceWith('¬'); return;
-    case TokenID.EQUIVALENT: this.replaceWith('⇔'); return;
-    case TokenID.GREATER_OR_EQ: this.replaceWith('≥'); return;
-    case TokenID.LESSER_OR_EQ: this.replaceWith('≤'); return;
-    case TokenID.PUNC_ASSIGN: this.replaceWith(':='); return;
-    case TokenID.PUNC_ITERATE: this.replaceWith(':∈'); return;
-
-    }
-  }
-};
\ No newline at end of file