def Lean.Server.FileWorker.noHighlightKinds : Array SyntaxNodeKind

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

Equations

• Lean.Server.FileWorker.noHighlightKinds = #[`Lean.Parser.Term.sorry, `Lean.Parser.Term.type, `Lean.Parser.Term.prop, `antiquotName]

def Lean.Server.FileWorker.docKinds : Array SyntaxNodeKind

Equations

• Lean.Server.FileWorker.docKinds = #[`Lean.Parser.Command.plainDocComment, `Lean.Parser.Command.docComment, `Lean.Parser.Command.moduleDoc]

def Lean.Server.FileWorker.keywordSemanticTokenMap : Std.TreeMap String Lsp.SemanticTokenType compare

Keywords for which a specific semantic token is provided.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Server.FileWorker.instBEqAbsoluteLspSemanticToken.beq x✝¹ x✝ = false

instance Lean.Server.FileWorker.instBEqAbsoluteLspSemanticToken : BEq AbsoluteLspSemanticToken

Equations

• Lean.Server.FileWorker.instBEqAbsoluteLspSemanticToken = { beq := Lean.Server.FileWorker.instBEqAbsoluteLspSemanticToken.beq }

instance Lean.Server.FileWorker.instHashableAbsoluteLspSemanticToken : Hashable AbsoluteLspSemanticToken

Equations

• Lean.Server.FileWorker.instHashableAbsoluteLspSemanticToken = { hash := Lean.Server.FileWorker.instHashableAbsoluteLspSemanticToken.hash }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Server.FileWorker.instFromJsonAbsoluteLspSemanticToken : FromJson AbsoluteLspSemanticToken

Equations

• Lean.Server.FileWorker.instFromJsonAbsoluteLspSemanticToken = { fromJson? := Lean.Server.FileWorker.instFromJsonAbsoluteLspSemanticToken.fromJson }

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

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Server.FileWorker.instToJsonAbsoluteLspSemanticToken : ToJson AbsoluteLspSemanticToken

Equations

• Lean.Server.FileWorker.instToJsonAbsoluteLspSemanticToken = { toJson := Lean.Server.FileWorker.instToJsonAbsoluteLspSemanticToken.toJson }

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Server.FileWorker.isVersoKind k = `Lean.Doc.Syntax.isPrefixOf k

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Server.FileWorker.SemanticTokensState : Type

instance Lean.Server.FileWorker.instTypeNameSemanticTokensState : TypeName SemanticTokensState

Equations

• Lean.Server.FileWorker.instTypeNameSemanticTokensState = Lean.Server.FileWorker.inst✝

instance Lean.Server.FileWorker.instInhabitedSemanticTokensState : Inhabited SemanticTokensState

Equations

• Lean.Server.FileWorker.instInhabitedSemanticTokensState = { default := Lean.Server.FileWorker.instInhabitedSemanticTokensState.default }

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

Equations

• Lean.Server.FileWorker.instInhabitedSemanticTokensState.default = { }

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

Computes all semantic tokens for the document.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Server.FileWorker.handleSemanticTokensDidChange x✝ = pure PUnit.unit

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

Computes the semantic tokens in the range provided by p.

Equations

• One or more equations did not get rendered due to their size.