@@ -6,6 +6,12 @@ export const TLA_OPERATORS = [
66 'E' , 'A' , 'X' , 'lnot' , 'land' , 'lor' , 'cdot' , 'equiv' , 'subseteq' , 'in' , 'notin' , 'intersect' ,
77 'union' , 'leq' , 'geq' , 'cup' , 'cap'
88] ;
9+ const TLA_UNICODE_OPERATORS : Map < string , string > = new Map ( [
10+ [ 'E' , '∃' ] , [ 'A' , '∀' ] , [ 'X' , '◊' ] , [ 'lnot' , '¬' ] , [ 'land' , '∧' ] , [ 'lor' , '∨' ] , [ 'cdot' , '·' ] ,
11+ [ 'equiv' , '≡' ] , [ 'subseteq' , '⊆' ] , [ 'in' , '∈' ] , [ 'notin' , '∉' ] , [ 'intersect' , '∩' ] ,
12+ [ 'union' , '∪' ] , [ 'leq' , '≤' ] , [ 'geq' , '≥' ] , [ 'cup' , '∪' ] , [ 'cap' , '∩' ]
13+ ] ) ;
14+
915export const TLA_STARTING_KEYWORDS = [ // These keywords start blocks, and should not be in the middle of an expression
1016 'EXTENDS' , 'VARIABLE' , 'VARIABLES' , 'CONSTANT' , 'CONSTANTS' , 'ASSUME' , 'ASSUMPTION' , 'AXIOM' , 'THEOREM' ,
1117 'PROOF' , 'LEMMA' , 'PROPOSITION' , 'COROLLARY' , 'RECURSIVE'
@@ -95,7 +101,7 @@ export class TlaCompletionItemProvider implements vscode.CompletionItemProvider
95101 item . insertText = item . label + ' ' ;
96102 break ;
97103 case vscode . CompletionItemKind . Operator :
98- item . insertText = item . label . toString ( ) . substring ( 1 ) + ' ' ;
104+ item . insertText = TLA_UNICODE_OPERATORS . get ( item . label . toString ( ) . substring ( 1 ) ) + ' ' ;
99105 break ;
100106 }
101107 return item ;
0 commit comments