def Lean.Server.FileWorker.noHighlightKinds : Array SyntaxNodeKind

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

def Lean.Server.FileWorker.docKinds : Array SyntaxNodeKind

def Lean.Server.FileWorker.keywordSemanticTokenMap : Std.TreeMap 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.

• priority : Nat

  In case of overlap, higher-priority tokens will take precendence

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.

• priority : Nat

  In case of overlap, higher-priority tokens will take precendence

def Lean.Server.FileWorker.instBEqAbsoluteLspSemanticToken.beq : AbsoluteLspSemanticToken → AbsoluteLspSemanticToken → Bool

@[implicit_reducible]

instance Lean.Server.FileWorker.instBEqAbsoluteLspSemanticToken : BEq AbsoluteLspSemanticToken

@[implicit_reducible]

instance Lean.Server.FileWorker.instHashableAbsoluteLspSemanticToken : Hashable AbsoluteLspSemanticToken

def Lean.Server.FileWorker.instHashableAbsoluteLspSemanticToken.hash : AbsoluteLspSemanticToken → UInt64

@[implicit_reducible]

instance Lean.Server.FileWorker.instFromJsonAbsoluteLspSemanticToken : FromJson AbsoluteLspSemanticToken

def Lean.Server.FileWorker.instFromJsonAbsoluteLspSemanticToken.fromJson : Json → Except String AbsoluteLspSemanticToken

def Lean.Server.FileWorker.instToJsonAbsoluteLspSemanticToken.toJson : AbsoluteLspSemanticToken → Json

@[implicit_reducible]

instance Lean.Server.FileWorker.instToJsonAbsoluteLspSemanticToken : ToJson AbsoluteLspSemanticToken

def Lean.Server.FileWorker.computeAbsoluteLspSemanticTokens (text : FileMap) (beginPos : String.Pos.Raw) (endPos? : Option String.Pos.Raw) (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.handleOverlappingSemanticTokens (tokens : Array AbsoluteLspSemanticToken) : Array AbsoluteLspSemanticToken

Eliminates overlapping tokens by selecting a single “best” token for each interval between token boundaries.

While LSP allows clients to state they they can handle overlapping tokens, widely used clients such as VS Code cannot handle them. Thus, we need to make them non-overlapping (this strictly generalizes removal of duplicates).

Given tokens A, B, C, D as in:

|-----A------|  |----D----|
    |------B----------|
        |----C----|

with priorities C > B, B > A, B > D, we want to emit the tokens:

|-A-|-B-|----C----|-B-|-D--|

In other words, B is split into two regions: before and after C.

If two overlapping tokens have the same priority, then ties are broken as follows:

• If the tokens start at the same position, then the shorter one is used.
• If they have the same start position and are the same length, then the one that occurs later in the original input array is used.
• If a new token starts in the middle of an existing one, and they have the same priority, then the new token is used.

Callers should ensure that all tokens in tokens designate non-empty regions of the file. In other words, it should be true that ∀ t ∈ tokens, t.pos < t.tailPos.

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.

def Lean.Server.FileWorker.isVersoKind (k : SyntaxNodeKind) : Bool

partial def Lean.Server.FileWorker.collectSyntaxBasedSemanticTokens (text : FileMap) (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.dbgShowTokens (text : FileMap) (toks : Array LeanSemanticToken) : String

A debugging utility for inspecting sets of collected tokens, classified by line and sorted by column.

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

structure Lean.Server.FileWorker.SemanticTokensState : Type

@[implicit_reducible]

instance Lean.Server.FileWorker.instTypeNameSemanticTokensState : TypeName SemanticTokensState

def Lean.Server.FileWorker.instInhabitedSemanticTokensState.default : SemanticTokensState

@[implicit_reducible]

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.