feat: Add semantic token highlighting

ProVerif · Mar 3, 2024 · ca39f7b · ca39f7b
1 parent 6a6ca86
commit ca39f7b
Show file tree

Hide file tree

Showing 4 changed files with 43 additions and 31 deletions.
diff --git a/server/src/semantic_token_provider.ts b/server/src/semantic_token_provider.ts
@@ -1,43 +1,51 @@
-import {integer, SemanticTokensBuilder} from 'vscode-languageserver';
+import {SemanticTokensBuilder} from 'vscode-languageserver';
 import {DocumentManagerInterface, ParseResult} from './document_manager';
-import {collectIdentTerminals, collectMatchingTerminals} from "./parseTree/collect_terminals";
-import {definitionSymbolsEqual, getDefinitionSymbolFromMatch} from "./go_to_definition";
+import {collectIdentTerminals} from "./parseTree/collect_terminals";
+import {getDefinitionSymbolFromMatch} from "./go_to_definition";
 import {nonNullable} from "./utils/array";
-import {notNull} from "antlr4ts/misc";
 import {DeclarationType} from "./tasks/create_symbol_table";
 
-export const tokenModifier = ['declaration', 'deprecated'];
-export const tokenTypes = ['function', 'variable', 'parameter', 'event'];
+export const tokenModifier = [];
+export const tokenTypes = ['function', 'variable', 'parameter'];
 
 export const getSemanticTokens = async (parseResult: ParseResult, documentManager: DocumentManagerInterface) => {
     // collect references
     const candidateTerminals = collectIdentTerminals(parseResult.parserTree);
     const terminalDefinitions = candidateTerminals
         .map(async terminal => getDefinitionSymbolFromMatch(parseResult, terminal, documentManager));
 
-	const tokensBuilder = new SemanticTokensBuilder();
+    const tokensBuilder = new SemanticTokensBuilder();
     (await Promise.all(terminalDefinitions))
-		.filter(nonNullable)
+        .filter(nonNullable)
         .forEach(terminalDefinition => {
-			const tokenType = getTokenType(terminalDefinition.symbol.declaration)
-			if (tokenType) {
-				const line = terminalDefinition.origin.match.symbol.line - 1;
-				const char = terminalDefinition.origin.match.symbol.charPositionInLine;
-				const length = terminalDefinition.origin.match.symbol.stopIndex - terminalDefinition.origin.match.symbol.startIndex + 1;
-				tokensBuilder.push(line, char, length, tokenType, [] as any)
-			}
+            const tokenType = getTokenType(terminalDefinition.symbol.declaration);
+            if (tokenType) {
+                const line = terminalDefinition.origin.match.symbol.line - 1;
+                const char = terminalDefinition.origin.match.symbol.charPositionInLine;
+                const length = terminalDefinition.origin.match.symbol.stopIndex - terminalDefinition.origin.match.symbol.startIndex + 1;
+                tokensBuilder.push(line, char, length, tokenType, [] as any);
+            }
         });
 
     return tokensBuilder.build();
 };
 
-const getTokenType = (declarationType: DeclarationType): number|undefined => {
-	switch (declarationType) {
-		case DeclarationType.Channel:
-		case DeclarationType.Free:
-		case DeclarationType.Const:
-			return tokenTypes.indexOf('variable')
-	}
+const getTokenType = (declarationType: DeclarationType): number | undefined => {
+    switch (declarationType) {
+        case DeclarationType.Channel:
+        case DeclarationType.Free:
+        case DeclarationType.Const:
+        case DeclarationType.Variable:
+            return tokenTypes.indexOf('variable');
+        case DeclarationType.Fun:
+        case DeclarationType.LetFun:
+        case DeclarationType.Event:
+            return tokenTypes.indexOf('function');
+        case DeclarationType.Parameter:
+        case DeclarationType.DefineParameter:
+        case DeclarationType.ExpandParameter:
+            return tokenTypes.indexOf('parameter');
+    }
 
-	return undefined
-}
+    return undefined;
+};
diff --git a/server/src/server.ts b/server/src/server.ts
@@ -126,8 +126,6 @@ connection.languages.semanticTokens.on(async params => {
         return new ResponseError(3, 'Semantic tokens extraction failed', undefined);
     }
 
-    console.log(semanticTokens)
-
     return semanticTokens;
 });
 

diff --git a/server/src/tasks/create_symbol_table.ts b/server/src/tasks/create_symbol_table.ts
@@ -29,6 +29,7 @@ export const createSymbolTable = (context: ParseTree): CreateSymbolTableResult =
 
 export enum DeclarationType {
     Parameter = 'parameter',
+    Variable = 'variable',
 
     Const = 'const',
     Channel = 'channel',
@@ -135,24 +136,24 @@ class SymbolTableVisitor extends AbstractParseTreeVisitor<ProverifSymbolTable> i
         return this.withContext(ctx, () => {
             if (ctx.LET() || ctx.IN()) {
                 collectTPattern(ctx.tpattern()).forEach(typedTerminal => {
-                    this.registerTypedTerminal(typedTerminal, DeclarationType.Parameter);
+                    this.registerTypedTerminal(typedTerminal, DeclarationType.Variable);
                 });
 
                 if (ctx.LET()) {
                     collectNevartype(ctx.nevartype()).forEach(typedTerminal => {
-                        this.registerTypedTerminal(typedTerminal, DeclarationType.Parameter);
+                        this.registerTypedTerminal(typedTerminal, DeclarationType.Variable);
                     });
                 }
             } else if (ctx.GET()) {
                 collectTPatternSeq(ctx.tpatternseq()).forEach(typedTerminal => {
-                    this.registerTypedTerminal(typedTerminal, DeclarationType.Parameter);
+                    this.registerTypedTerminal(typedTerminal, DeclarationType.Variable);
                 });
             } else if (ctx.NEW() || ctx.RANDOM()) {
                 const type = getType(ctx.typeid());
-                this.registerTerminal(ctx.IDENT()[0], DeclarationType.Parameter, type);
+                this.registerTerminal(ctx.IDENT()[0], DeclarationType.Variable, type);
             } else if (ctx.LEFTARROW()) {
                 const typedTerminal = collectBasicpattern(ctx.basicpattern());
-                this.registerTypedTerminal(typedTerminal, DeclarationType.Parameter);
+                this.registerTypedTerminal(typedTerminal, DeclarationType.Variable);
             }
 
             return this.visitChildren(ctx);

diff --git a/syntaxes/pv.tmLanguage.json b/syntaxes/pv.tmLanguage.json
@@ -298,6 +298,11 @@
           "end": "(?=})",
           "patterns" : [{ "include": "$self"}]
         },
+        {
+          "begin" : "\\(",
+          "end"   : "\\)",
+          "patterns" : [{ "include": "#comments"}]
+        },
         { "include": "#fun_ident" }
       ]
     },