Add Unicode Operator completions

package.json

@@ -584,6 +584,12 @@
                     "default": false,
                     "markdownDescription": "Enable the knowledge-base *tools* in the MCP server in addition to the knowledge-base *resources*. The two tools tlaplus_mcp_knowledge_list and tlaplus_mcp_knowledge_get allow you to search and read TLA+ knowledge-base articles as MCP tools. Restart VSCode to apply the changes. You’ll rarely need to enable this option, since both VSCode and Cursor already support MCP resources."
                 },
+                "tlaplus.unicode.autocomplete": {
+                    "type": "boolean",
+                    "scope": "window",
+                    "default": false,
+                    "markdownDescription": "Enable Unicode autocomplete in the editor. Requires reload to update."
+                },
                 "tlaplus.pdf.convertCommand": {
                     "default": "pdflatex",
                     "type": "string",

src/completions/tlaCompletions.ts

@@ -3,9 +3,64 @@
 import { getPrevText } from './completions';
 
 export const TLA_OPERATORS = [
-    'E', 'A', 'X', 'lnot', 'land', 'lor', 'cdot', 'equiv', 'subseteq', 'in', 'notin', 'intersect',
-    'union', 'leq', 'geq', 'cup', 'cap'
+    'land',                    'lor',                 'implies',
+    'lnot',                    'equiv',               'equiv',
+    'in',                      'notin',               'ne',
+    'll',                      'gg',                  '[]',
+    'leq',                     'geq',                 '<>',
+    'll',                      'gg',                  '~>',
+    'prec',                    'succ',                '-+->',
+    'preceq',                  'succeq',              'div',
+    'subseteq',                'supseteq',            'cdot',
+    'subset',                  'supset',              'o',
+    'sqsubset',                'sqsupset',            'bullet',
+    'sqsubseteq',              'sqsupseteq',          'star',
+    'vdash',                   'dashv',               'bigcirc',
+    'models',                  'vDash',               'sim',
+    'maps',                    'leftarrow',           'simeq',
+    'cap',                     'cup',                 'asymp',
+    'sqcap',                   'sqcup',               'approx',
+    'oplus',                   'uplus',               'cong',
+    'ominus',                  'X',                   'doteq',
+    'odot',                    'wr',
+    'otimes',                  'propto',
+    'oslash',                  's',
+    'E',                       'A',
+    'EE',                      'AA'
 ];
+
+const enableUnicodeAutocomplete = vscode.workspace.getConfiguration()
+    .get<boolean>('tlaplus.unicode.autocomplete', false);
+
+const TLA_UNICODE_OPERATORS: Map<string, string> = new Map([
+    ['land', '∧'],           ['lor', '∨'],            ['implies', '⇒'],
+    ['lnot', '¬'],           ['equiv', '≡'],          ['triangleq', '≜'],
+    ['in', '∈'],             ['notin', '∉'],          ['ne', '≠'],
+    ['ll', '≪'],             ['gg', '≫'],             ['[]', '□'],
+    ['leq', '≤'],            ['geq', '≥'],            ['<>', '◊'],
+    ['ll', '≪'],             ['gg', '≫'],             ['~>', '↝'],
+    ['prec', '≺'],           ['succ', '≻'],           ['-+->', '⇸'],
+    ['preceq', '⪯'],         ['succeq', '⪰'],         ['div', '÷'],
+    ['subseteq', '⊆'],       ['supseteq', '⊇'],       ['cdot', '·'],
+    ['subset', '⊂'],         ['supset', '⊃'],         ['o', '○'],
+    ['sqsubset', '⊏'],       ['sqsupset', '⊐'],       ['bullet', '•'],
+    ['sqsubseteq', '⊑'],     ['sqsupseteq', '⊒'],     ['star', '⋆'],
+    ['vdash', '⊢'],          ['dashv', '⊣'],          ['bigcirc', '◯'],
+    ['models', '⊨'],         ['vDash', '=|'],         ['sim', '∼'],
+    ['maps', '→'],           ['leftarrow', '←'],      ['simeq', '≃'],
+    ['cap', '∩'],            ['cup', '∪'],            ['asymp', '≍'],
+    ['sqcap', '⊓'],          ['sqcup', '⊔'],          ['approx', '≈'],
+    ['oplus', '⊕'],          ['uplus', '⊎'],          ['cong', '≅'],
+    ['ominus', '⊖'],         ['X', '×'],              ['doteq', '≐'],
+    ['odot', '⊙'],           ['wr', '≀'],
+    ['otimes', '⊗'],         ['propto', '∝'],
+    ['oslash', '⊘'],
+    ['E', '∃'],              ['A', '∀'],
+    ['EE', '∃'],             ['AA', '∀'],
+    // Repeats
+    ['times', '×'], ['circ', '∘'], ['intersect', '∩'], ['union', '∪'],
+]);
+
 export const TLA_STARTING_KEYWORDS = [  // These keywords start blocks, and should not be in the middle of an expression
     'EXTENDS', 'VARIABLE', 'VARIABLES', 'CONSTANT', 'CONSTANTS', 'ASSUME', 'ASSUMPTION', 'AXIOM', 'THEOREM',
     'PROOF', 'LEMMA', 'PROPOSITION', 'COROLLARY', 'RECURSIVE'
@@ -95,7 +150,9 @@
                 item.insertText = item.label + ' ';
                 break;
             case vscode.CompletionItemKind.Operator:
-                item.insertText = item.label.toString().substring(1) + ' ';
+                item.insertText = enableUnicodeAutocomplete ?
+                    TLA_UNICODE_OPERATORS.get(item.label.toString().substring(1)) + ' ' :
+                    item.label.toString().substring(1) + ' ';
                 break;
         }
         return item;