Semantic tokens highlighting #2919
Conversation
# Conflicts: # Source/Dafny/AST/DafnyAst.cs # Source/DafnyCore/Coco/Scanner.frame # Source/DafnyCore/Dafny.atg
| @@ -328,6 +328,7 @@ abstract public class ModuleDecl : TopLevelDecl { | |||
| return Signature; | |||
| } | |||
| public int Height; | |||
| public Token RootToken = new Token(); | |||
There was a problem hiding this comment.
Root sounds like a tree is involved, but IIUC the tokens form a list not a tree. How about FirstToken as a name?
Source/DafnyCore/Dafny.atg
Outdated
| Comment | ||
| } | ||
|
|
||
| private static TokenClass ClassifyToken(int kind) { // FIXME rewrite as a dictionary of lists |
There was a problem hiding this comment.
Please resolve the FIXME
| #pragma warning disable CS8524 | ||
| // [CS8524] The switch expression does not handle some values of its input type (it is not exhaustive) involving | ||
| // an unnamed enum value. For example, the pattern '(Microsoft.Dafny.Parser.TokenClass)16' is not covered. | ||
| Parser.TokenClassificationMap[tok.kind] switch { |
There was a problem hiding this comment.
Why do we first map to Parser.TokenClass and then to (SemanticTokenType? tokenType, SemanticTokenModifier[] modifiers), instead of skipping Parser.TokenClass ?
There was a problem hiding this comment.
There are two levels of abstraction here. TokenClass regroups tokens by more classes than SemanticTokenType, so that it will be easier to migrate groups to new semantics tokens when they appear.
| var importNameTokens = | ||
| await ParseAndCollectTokens("module M {} module N { import M' = M }"); | ||
|
|
||
| // FIXME |
| logger.LogWarning("Tokens requested for unloaded document {DocumentUri}", identifier.TextDocument.Uri); | ||
| return; | ||
| } | ||
| var document = await documentManager.GetLastDocumentAsync(); |
There was a problem hiding this comment.
Please don't use GetLastDocumentAsync. There's no need to wait for verification to have completed. I think we need a GetParsedDocumentAsync, although using GetResolvedDocumentAsync would already be better.
| }; | ||
| } | ||
|
|
||
| private void CollectBasicTokens(DafnySemanticTokensBuilder builder, Dafny.Program program) { |
There was a problem hiding this comment.
Basic doesn't mean much to me, and I think Semantic in CollectSemanticTokens is incorrect because I would say parsing doesn't establish semantics, even though LSP mentions the word Semantic in many of its token related classes (that we are also using for the 'Basic' tokens).
I'm not sure about the names though. Maybe PushTokensBasedOnLexing and PushTokensBasedOnParsing
There was a problem hiding this comment.
Renamed to "CollectScannerTokens" and "CollectResolutionBasedTokens"
| } | ||
|
|
||
| public override void Visit(LiteralExpr literalExpression) { | ||
| //# builder.Push("literalExpression", literalExpression.tok, SemanticTokenType.Macro, SemanticTokenModifier.DefaultLibrary); //?Macro |
| } | ||
|
|
||
| public override void VisitUnknown(object node, IToken token) { | ||
| // FIXME change to logging a warning |
| // FIXME change to logging a warning | ||
| } | ||
|
|
||
| public override void Visit(ModuleDefinition moduleDefinition) { // TODO Keyword token |
| /// <summary> | ||
| /// Visitor responsible for populating a table of document tokens. | ||
| /// </summary> | ||
| public class LspSemanticTokensGeneratingVisitor : SyntaxTreeVisitor { |
There was a problem hiding this comment.
Would it be possible to replace this visitor with an interface IHasHighlight { bool Highlight(DafnySemanticTokensBuilder builder) that the individual Node classes can implement ?
There was a problem hiding this comment.
Would it be possible to replace this visitor with an interface IHasHighlight { bool Highlight(DafnySemanticTokensBuilder builder) that the individual Node classes can implement ?
That would require to make DafnyCore aware of the language server, so I wouldn't go that route.
Before
After
Fixes dafny-lang/ide-vscode#299
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.