From a29a91eadabe26a361d94958e4aeb756bee6c158 Mon Sep 17 00:00:00 2001 From: miguelraz Date: Sun, 30 Nov 2025 11:50:56 -0600 Subject: [PATCH 1/4] Add Unicode Operator completions Signed-off-by: miguelraz --- src/completions/tlaCompletions.ts | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/completions/tlaCompletions.ts b/src/completions/tlaCompletions.ts index c6840de8..c3901fbc 100644 --- a/src/completions/tlaCompletions.ts +++ b/src/completions/tlaCompletions.ts @@ -6,6 +6,12 @@ export const TLA_OPERATORS = [ 'E', 'A', 'X', 'lnot', 'land', 'lor', 'cdot', 'equiv', 'subseteq', 'in', 'notin', 'intersect', 'union', 'leq', 'geq', 'cup', 'cap' ]; +const TLA_UNICODE_OPERATORS: Map = new Map([ + ['E', '∃'], ['A', '∀'], ['X', '◊'], ['lnot', '¬'], ['land', '∧'], ['lor', '∨'], ['cdot', '·'], + ['equiv', '≡'], ['subseteq', '⊆'], ['in', '∈'], ['notin', '∉'], ['intersect', '∩'], + ['union', '∪'], ['leq', '≤'], ['geq', '≥'], ['cup', '∪'], ['cap', '∩'] +]); + 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 +101,7 @@ export class TlaCompletionItemProvider implements vscode.CompletionItemProvider item.insertText = item.label + ' '; break; case vscode.CompletionItemKind.Operator: - item.insertText = item.label.toString().substring(1) + ' '; + item.insertText = TLA_UNICODE_OPERATORS.get(item.label.toString().substring(1)) + ' '; break; } return item; From 23987e61b7a0a41835db8080f57ceea01f81b7f9 Mon Sep 17 00:00:00 2001 From: miguelraz Date: Sun, 30 Nov 2025 20:31:01 -0600 Subject: [PATCH 2/4] Add Unicode Autocomplete configuration checkbox defaulting to false Signed-off-by: miguelraz --- package.json | 6 ++++++ src/completions/tlaCompletions.ts | 8 +++++++- 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/package.json b/package.json index 30d4cad5..18330dfc 100644 --- a/package.json +++ b/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", diff --git a/src/completions/tlaCompletions.ts b/src/completions/tlaCompletions.ts index c3901fbc..7e2696c7 100644 --- a/src/completions/tlaCompletions.ts +++ b/src/completions/tlaCompletions.ts @@ -6,6 +6,10 @@ export const TLA_OPERATORS = [ 'E', 'A', 'X', 'lnot', 'land', 'lor', 'cdot', 'equiv', 'subseteq', 'in', 'notin', 'intersect', 'union', 'leq', 'geq', 'cup', 'cap' ]; + +const enableUnicodeAutocomplete = vscode.workspace.getConfiguration() + .get('tlaplus.unicode.autocomplete', false); + const TLA_UNICODE_OPERATORS: Map = new Map([ ['E', '∃'], ['A', '∀'], ['X', '◊'], ['lnot', '¬'], ['land', '∧'], ['lor', '∨'], ['cdot', '·'], ['equiv', '≡'], ['subseteq', '⊆'], ['in', '∈'], ['notin', '∉'], ['intersect', '∩'], @@ -101,7 +105,9 @@ export class TlaCompletionItemProvider implements vscode.CompletionItemProvider item.insertText = item.label + ' '; break; case vscode.CompletionItemKind.Operator: - item.insertText = TLA_UNICODE_OPERATORS.get(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; From 80fb8168a78722fd0646fead886183ada65289e7 Mon Sep 17 00:00:00 2001 From: miguelraz Date: Sun, 30 Nov 2025 23:02:31 -0600 Subject: [PATCH 3/4] Add all Unicode from ASCII Representation of Typeset Symbols to Autocompletions The formatting of the consts TLA_UNICODE_OPERATORS and TLA_OPERATORS was done with the assistance of Claude Sonnet 4. Signed-off-by: miguelraz --- src/completions/tlaCompletions.ts | 55 ++++++++++++++++++++++++++++--- 1 file changed, 50 insertions(+), 5 deletions(-) diff --git a/src/completions/tlaCompletions.ts b/src/completions/tlaCompletions.ts index 7e2696c7..8926709f 100644 --- a/src/completions/tlaCompletions.ts +++ b/src/completions/tlaCompletions.ts @@ -3,17 +3,62 @@ import { TlaDocumentInfos } from '../model/documentInfo'; 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('tlaplus.unicode.autocomplete', false); const TLA_UNICODE_OPERATORS: Map = new Map([ - ['E', '∃'], ['A', '∀'], ['X', '◊'], ['lnot', '¬'], ['land', '∧'], ['lor', '∨'], ['cdot', '·'], - ['equiv', '≡'], ['subseteq', '⊆'], ['in', '∈'], ['notin', '∉'], ['intersect', '∩'], - ['union', '∪'], ['leq', '≤'], ['geq', '≥'], ['cup', '∪'], ['cap', '∩'] + ['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 From c0109664a68dcc6c1336245fa63cbbf07de26b9b Mon Sep 17 00:00:00 2001 From: miguelraz Date: Mon, 1 Dec 2025 22:13:12 -0600 Subject: [PATCH 4/4] Add all 3 columns of accepted TLA+ Unicode symbols Signed-off-by: miguelraz --- src/completions/tlaCompletions.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/completions/tlaCompletions.ts b/src/completions/tlaCompletions.ts index 8926709f..ec6b69af 100644 --- a/src/completions/tlaCompletions.ts +++ b/src/completions/tlaCompletions.ts @@ -46,7 +46,7 @@ const TLA_UNICODE_OPERATORS: Map = new Map([ ['sqsubset', '⊏'], ['sqsupset', '⊐'], ['bullet', '•'], ['sqsubseteq', '⊑'], ['sqsupseteq', '⊒'], ['star', '⋆'], ['vdash', '⊢'], ['dashv', '⊣'], ['bigcirc', '◯'], - ['models', '⊨'], ['vDash', '=|'], ['sim', '∼'], + ['models', '⊨'], ['vDash', '=|'], ['sim', '∼'], ['maps', '→'], ['leftarrow', '←'], ['simeq', '≃'], ['cap', '∩'], ['cup', '∪'], ['asymp', '≍'], ['sqcap', '⊓'], ['sqcup', '⊔'], ['approx', '≈'],