SyntaxNodeKind
s for which the syntax node and its children receive no semantic highlighting.
Equations
Instances For
Keywords for which a specific semantic token is provided.
Equations
Instances For
Semantic token information for a given Syntax
.
- stx : Syntax
Syntax of the semantic token.
- type : Lsp.SemanticTokenType
Type of the semantic token.
Instances For
Semantic token information with absolute LSP positions.
- pos : Lsp.Position
Start position of the semantic token.
- tailPos : Lsp.Position
End position of the semantic token.
- type : Lsp.SemanticTokenType
Start position of the semantic token.
Instances For
Given a set of LeanSemanticToken
, computes the AbsoluteLspSemanticToken
with absolute
LSP position information for each token.
Equations
Instances For
Filters all duplicate semantic tokens with the same pos
, tailPos
and type
.
Equations
Instances For
Given a set of AbsoluteLspSemanticToken
, computes the LSP SemanticTokens
data with
token-relative positioning.
See https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_semanticTokens.
Equations
Instances For
Collects all semantic tokens that can be deduced purely from Syntax
without elaboration information.
Collects all semantic tokens from the given Elab.InfoTree
.
Equations
Instances For
Equations
Instances For
Computes all semantic tokens for the document.
Equations
Instances For
Computes the semantic tokens in the range provided by p
.