def Lean.Server.FileWorker.noHighlightKinds : Array SyntaxNodeKind

SyntaxNodeKinds for which the syntax node and its children receive no semantic highlighting.

def Lean.Server.FileWorker.keywordSemanticTokenMap : RBMap String Lsp.SemanticTokenType compare

Keywords for which a specific semantic token is provided.

structure Lean.Server.FileWorker.LeanSemanticToken : Type

Semantic token information for a given Syntax.

• stx : Syntax

  Syntax of the semantic token.

• type : Lsp.SemanticTokenType

  Type of the semantic token.

structure Lean.Server.FileWorker.AbsoluteLspSemanticToken : Type

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.

instance Lean.Server.FileWorker.instBEqAbsoluteLspSemanticToken : BEq AbsoluteLspSemanticToken

instance Lean.Server.FileWorker.instHashableAbsoluteLspSemanticToken : Hashable AbsoluteLspSemanticToken

instance Lean.Server.FileWorker.instFromJsonAbsoluteLspSemanticToken : FromJson AbsoluteLspSemanticToken

instance Lean.Server.FileWorker.instToJsonAbsoluteLspSemanticToken : ToJson AbsoluteLspSemanticToken

def Lean.Server.FileWorker.computeAbsoluteLspSemanticTokens (text : FileMap) (beginPos : String.Pos) (endPos? : Option String.Pos) (tokens : Array LeanSemanticToken) : Array AbsoluteLspSemanticToken

Given a set of LeanSemanticToken, computes the AbsoluteLspSemanticToken with absolute LSP position information for each token.

def Lean.Server.FileWorker.filterDuplicateSemanticTokens (tokens : Array AbsoluteLspSemanticToken) : Array AbsoluteLspSemanticToken

Filters all duplicate semantic tokens with the same pos, tailPos and type.

def Lean.Server.FileWorker.computeDeltaLspSemanticTokens (tokens : Array AbsoluteLspSemanticToken) : Lsp.SemanticTokens

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.

partial def Lean.Server.FileWorker.collectSyntaxBasedSemanticTokens (stx : Syntax) : Array LeanSemanticToken

Collects all semantic tokens that can be deduced purely from Syntax without elaboration information.

def Lean.Server.FileWorker.collectInfoBasedSemanticTokens (i : Elab.InfoTree) : Array LeanSemanticToken

Collects all semantic tokens from the given Elab.InfoTree.

def Lean.Server.FileWorker.computeSemanticTokens (doc : EditableDocument) (beginPos : String.Pos) (endPos? : Option String.Pos) (snaps : List Snapshots.Snapshot) : RequestM Lsp.SemanticTokens

structure Lean.Server.FileWorker.SemanticTokensState : Type

instance Lean.Server.FileWorker.instTypeNameSemanticTokensState : TypeName SemanticTokensState

instance Lean.Server.FileWorker.instInhabitedSemanticTokensState : Inhabited SemanticTokensState

def Lean.Server.FileWorker.handleSemanticTokensFull : Lsp.SemanticTokensParams → SemanticTokensState → RequestM (LspResponse Lsp.SemanticTokens × SemanticTokensState)

Computes all semantic tokens for the document.

def Lean.Server.FileWorker.handleSemanticTokensDidChange : Lsp.DidChangeTextDocumentParams → StateT SemanticTokensState RequestM Unit

def Lean.Server.FileWorker.handleSemanticTokensRange (p : Lsp.SemanticTokensRangeParams) : RequestM (RequestTask Lsp.SemanticTokens)

Computes the semantic tokens in the range provided by p.