def Lean.Server.FileWorker.noHighlightKinds : Array SyntaxNodeKind

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

Equations

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

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.

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.

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

Equations

• Lean.Server.FileWorker.instBEqAbsoluteLspSemanticToken.beq { pos := a, tailPos := a_1, type := a_2 } { pos := b, tailPos := b_1, type := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• 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 }

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

Equations

• Lean.Server.FileWorker.instHashableAbsoluteLspSemanticToken.hash { pos := a, tailPos := a_1, type := a_2 } = mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)

instance Lean.Server.FileWorker.instHashableAbsoluteLspSemanticToken : Hashable AbsoluteLspSemanticToken

Equations

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

instance Lean.Server.FileWorker.instFromJsonAbsoluteLspSemanticToken : FromJson AbsoluteLspSemanticToken

Equations

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

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

Equations

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

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) (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.

Equations

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

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

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

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.

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.

Equations

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

def Lean.Server.FileWorker.computeSemanticTokens (doc : EditableDocument) (beginPos : String.Pos) (endPos? : Option String.Pos) (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✝

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

Equations

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

instance Lean.Server.FileWorker.instInhabitedSemanticTokensState : Inhabited SemanticTokensState

Equations

• Lean.Server.FileWorker.instInhabitedSemanticTokensState = { default := 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.