diff --git a/server/src/parseTree/collect_matching_terminals.ts b/server/src/parseTree/collect_terminals.ts similarity index 51% rename from server/src/parseTree/collect_matching_terminals.ts rename to server/src/parseTree/collect_terminals.ts index 66ea68c..7c1434c 100644 --- a/server/src/parseTree/collect_matching_terminals.ts +++ b/server/src/parseTree/collect_terminals.ts @@ -1,5 +1,6 @@ import {ParseTree, TerminalNode} from "antlr4ts/tree"; import {ParserRuleContext} from "antlr4ts"; +import {ProverifParser} from "../parser-proverif/ProverifParser"; export const collectMatchingTerminals = (parseTree: ParseTree, text: string): TerminalNode[] => { if (parseTree instanceof TerminalNode) { @@ -20,3 +21,23 @@ export const collectMatchingTerminals = (parseTree: ParseTree, text: string): Te return matchingTerminals; }; + +export const collectIdentTerminals = (parseTree: ParseTree): TerminalNode[] => { + if (parseTree instanceof TerminalNode) { + const token = parseTree.symbol; + if (token.type === ProverifParser.IDENT) { + return [parseTree]; + } + } + + const matchingTerminals: TerminalNode[] = []; + if (parseTree instanceof ParserRuleContext) { + // check if children match + for (let i = 0; i < parseTree.childCount; i++) { + const matchingTerminalsChild = collectIdentTerminals(parseTree.getChild(i)); + matchingTerminals.push(...matchingTerminalsChild); + } + } + + return matchingTerminals; +}; diff --git a/server/src/references.ts b/server/src/references.ts index 690eb8f..5c74637 100644 --- a/server/src/references.ts +++ b/server/src/references.ts @@ -6,7 +6,7 @@ import { getDefinitionSymbolFromMatch, getDefinitionSymbolFromPosition } from "./go_to_definition"; -import {collectMatchingTerminals} from "./parseTree/collect_matching_terminals"; +import {collectMatchingTerminals} from "./parseTree/collect_terminals"; import {ParseTree} from "antlr4ts/tree"; import {getRange} from "./parseTree/get_range"; import {nonNullable} from "./utils/array"; diff --git a/server/src/semantic_token_provider.ts b/server/src/semantic_token_provider.ts index 88acd5d..bb75e4d 100644 --- a/server/src/semantic_token_provider.ts +++ b/server/src/semantic_token_provider.ts @@ -1,14 +1,43 @@ -import {SemanticTokensBuilder} from 'vscode-languageserver'; -import {ParseResult} from './document_manager'; +import {integer, 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 {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 getSemanticTokens = (parseResult: ParseResult) => { - // solely for demonstration purposes - const tokensBuilder = new SemanticTokensBuilder(); - tokensBuilder.push(9, 8, 1, tokenTypes.indexOf('variable'), [tokenModifier.indexOf('deprecated')] as any); - tokensBuilder.push(10, 8, 1, tokenTypes.indexOf('variable'), [] as any); - tokensBuilder.push(10, 11, 1, tokenTypes.indexOf('variable'), tokenModifier.indexOf('deprecated')); +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(); + (await Promise.all(terminalDefinitions)) + .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) + } + }); + return tokensBuilder.build(); -}; \ No newline at end of file +}; + +const getTokenType = (declarationType: DeclarationType): number|undefined => { + switch (declarationType) { + case DeclarationType.Channel: + case DeclarationType.Free: + case DeclarationType.Const: + return tokenTypes.indexOf('variable') + } + + return undefined +} \ No newline at end of file diff --git a/server/src/server.ts b/server/src/server.ts index 44e01e3..37dba9e 100644 --- a/server/src/server.ts +++ b/server/src/server.ts @@ -13,7 +13,7 @@ import {DocumentManager, DocumentManagerInterface,} from "./document_manager"; import {getDefinitionLink} from "./go_to_definition"; import {rename} from "./rename"; import {getReferences} from "./references"; -import {getSemanticTokens} from './semantic_token_provider'; +import {getSemanticTokens, tokenModifier, tokenTypes} from './semantic_token_provider'; import {getDocumentLinks} from "./document_links"; import {getSignatureHelp} from "./signature_help"; import {getHover} from "./hover"; @@ -45,15 +45,13 @@ connection.onInitialize((params: InitializeParams) => { referencesProvider: true, renameProvider: true, signatureHelpProvider: { triggerCharacters: ['('], retriggerCharacters: [',', ', '] }, - hoverProvider: true - /** + hoverProvider: true, semanticTokensProvider: { documentSelector: null, // use client-side definition legend: {tokenModifiers: tokenModifier, tokenTypes: tokenTypes}, full: true, range: false }, - **/ }, }; @@ -122,12 +120,14 @@ connection.languages.semanticTokens.on(async params => { return new ResponseError(2, 'Parsing failed', undefined); } - const semanticTokens = getSemanticTokens(parseResult); + const semanticTokens = await getSemanticTokens(parseResult, documentManager); if (!semanticTokens) { connection.console.error("Retrieving semantic tokens failed."); return new ResponseError(3, 'Semantic tokens extraction failed', undefined); } + console.log(semanticTokens) + return semanticTokens; });