Add Unicode Autocomplete configuration checkbox defaulting to false

Signed-off-by: miguelraz <miguelraz@ciencias.unam.mx>

Author: miguelraz

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

@@ -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<boolean>('tlaplus.unicode.autocomplete', false);
+
 const TLA_UNICODE_OPERATORS: Map<string, string> = 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;