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 : RBMap 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.

instance Lean.Server.FileWorker.instBEqAbsoluteLspSemanticToken : BEq AbsoluteLspSemanticToken

Equations

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

instance Lean.Server.FileWorker.instHashableAbsoluteLspSemanticToken : Hashable AbsoluteLspSemanticToken

Equations

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

instance Lean.Server.FileWorker.instFromJsonAbsoluteLspSemanticToken : FromJson AbsoluteLspSemanticToken

Equations

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

instance Lean.Server.FileWorker.instToJsonAbsoluteLspSemanticToken : ToJson AbsoluteLspSemanticToken

Equations

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

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✝

instance Lean.Server.FileWorker.instInhabitedSemanticTokensState : Inhabited 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.