def Lean.Server.FileWorker.findCompletionCmdDataAtPos (doc : Lean.Server.FileWorker.EditableDocument) (pos : String.Pos) : Task (Option (Lean.Syntax × Lean.Elab.InfoTree))

Equations

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

def Lean.Server.FileWorker.handleCompletion (p : Lean.Lsp.CompletionParams) : Lean.Server.RequestM (Lean.Server.RequestTask Lean.Lsp.CompletionList)

def Lean.Server.FileWorker.handleCompletionItemResolve (item : Lean.Lsp.CompletionItem) : Lean.Server.RequestM (Lean.Server.RequestTask Lean.Lsp.CompletionItem)

Handles completionItem/resolve requests that are sent by the client after the user selects a completion item that was provided by textDocument/completion. Resolving the item fills the detail? field of the item with the pretty-printed type. This control flow is necessary because pretty-printing the type for every single completion item (even those never selected by the user) is inefficient.

def Lean.Server.FileWorker.handleHover (p : Lean.Lsp.HoverParams) : Lean.Server.RequestM (Lean.Server.RequestTask (Option Lean.Lsp.Hover))

Equations

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

def Lean.Server.FileWorker.locationLinksOfInfo (kind : Lean.Server.GoToKind) (ictx : Lean.Elab.InfoWithCtx) (infoTree? : Option Lean.Elab.InfoTree := none) : Lean.Server.RequestM (Array Lean.Lsp.LocationLink)

def Lean.Server.FileWorker.locationLinksOfInfo.extractInstances (i : Lean.Elab.Info) (ci : Lean.Elab.ContextInfo) : Lean.Expr → Lean.Server.RequestM (Array Lean.Name)

def Lean.Server.FileWorker.handleDefinition (kind : Lean.Server.GoToKind) (p : Lean.Lsp.TextDocumentPositionParams) : Lean.Server.RequestM (Lean.Server.RequestTask (Array Lean.Lsp.LocationLink))

Equations

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

def Lean.Server.FileWorker.getInteractiveGoals (p : Lean.Lsp.PlainGoalParams) : Lean.Server.RequestM (Lean.Server.RequestTask (Option Lean.Widget.InteractiveGoals))

def Lean.Server.FileWorker.handlePlainGoal (p : Lean.Lsp.PlainGoalParams) : Lean.Server.RequestM (Lean.Server.RequestTask (Option Lean.Lsp.PlainGoal))

def Lean.Server.FileWorker.getInteractiveTermGoal (p : Lean.Lsp.PlainTermGoalParams) : Lean.Server.RequestM (Lean.Server.RequestTask (Option Lean.Widget.InteractiveTermGoal))

def Lean.Server.FileWorker.handlePlainTermGoal (p : Lean.Lsp.PlainTermGoalParams) : Lean.Server.RequestM (Lean.Server.RequestTask (Option Lean.Lsp.PlainTermGoal))

def Lean.Server.FileWorker.handleDocumentHighlight (p : Lean.Lsp.DocumentHighlightParams) : Lean.Server.RequestM (Lean.Server.RequestTask (Array Lean.Lsp.DocumentHighlight))

partial def Lean.Server.FileWorker.handleDocumentHighlight.highlightReturn? (text : Lean.FileMap) (pos : String.Pos) (doRange? : Option Lean.Lsp.Range) : Lean.Syntax → Option Lean.Lsp.DocumentHighlight

structure Lean.Server.FileWorker.NamespaceEntry : Type

• name : List Lean.Name

  The list of the name components introduced by this namespace command, in reverse order so that end will peel them off from the front.

• stx : Lean.Syntax
• selection : Lean.Syntax
• prevSiblings : Array Lean.Lsp.DocumentSymbol

def Lean.Server.FileWorker.NamespaceEntry.finish (text : Lean.FileMap) (syms : Array Lean.Lsp.DocumentSymbol) (endStx : Option Lean.Syntax) : Lean.Server.FileWorker.NamespaceEntry → Array Lean.Lsp.DocumentSymbol

def Lean.Server.FileWorker.handleDocumentSymbol : Lean.Lsp.DocumentSymbolParams → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Lsp.DocumentSymbolResult)

Equations

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

partial def Lean.Server.FileWorker.handleDocumentSymbol.toDocumentSymbols (text : Lean.FileMap) (stxs : List Lean.Syntax) (syms : Array Lean.Lsp.DocumentSymbol) (stack : List Lean.Server.FileWorker.NamespaceEntry) : Array Lean.Lsp.DocumentSymbol

partial def Lean.Server.FileWorker.handleDocumentSymbol.toDocumentSymbols.popStack (text : Lean.FileMap) (stx : Lean.Syntax) (stxs : List Lean.Syntax) (n : Nat) (syms : Array Lean.Lsp.DocumentSymbol) : List Lean.Server.FileWorker.NamespaceEntry → Array Lean.Lsp.DocumentSymbol

def Lean.Server.FileWorker.noHighlightKinds : Array Lean.SyntaxNodeKind

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

def Lean.Server.FileWorker.keywordSemanticTokenMap : Lean.RBMap String Lean.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 : Lean.Syntax

  Syntax of the semantic token.

• type : Lean.Lsp.SemanticTokenType

  Type of the semantic token.

structure Lean.Server.FileWorker.AbsoluteLspSemanticToken : Type

Semantic token information with absolute LSP positions.

• pos : Lean.Lsp.Position

  Start position of the semantic token.

• tailPos : Lean.Lsp.Position

  End position of the semantic token.

• type : Lean.Lsp.SemanticTokenType

  Start position of the semantic token.

instance Lean.Server.FileWorker.instBEqAbsoluteLspSemanticToken : BEq Lean.Server.FileWorker.AbsoluteLspSemanticToken

Equations

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

instance Lean.Server.FileWorker.instHashableAbsoluteLspSemanticToken : Hashable Lean.Server.FileWorker.AbsoluteLspSemanticToken

Equations

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

instance Lean.Server.FileWorker.instFromJsonAbsoluteLspSemanticToken : Lean.FromJson Lean.Server.FileWorker.AbsoluteLspSemanticToken

Equations

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

instance Lean.Server.FileWorker.instToJsonAbsoluteLspSemanticToken : Lean.ToJson Lean.Server.FileWorker.AbsoluteLspSemanticToken

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

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

def Lean.Server.FileWorker.collectInfoBasedSemanticTokens (i : Lean.Elab.InfoTree) : Array Lean.Server.FileWorker.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.handleSemanticTokens (beginPos : String.Pos) (endPos? : Option String.Pos) : Lean.Server.RequestM (Lean.Server.RequestTask Lean.Lsp.SemanticTokens)

Computes the semantic tokens in the range [beginPos, endPos?).

Equations

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

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

Equations

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

def Lean.Server.FileWorker.handleSemanticTokensFull : Lean.Lsp.SemanticTokensParams → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Lsp.SemanticTokens)

Computes all semantic tokens for the document.

def Lean.Server.FileWorker.handleSemanticTokensRange (p : Lean.Lsp.SemanticTokensRangeParams) : Lean.Server.RequestM (Lean.Server.RequestTask Lean.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.

def Lean.Server.FileWorker.handleFoldingRange : Lean.Lsp.FoldingRangeParams → Lean.Server.RequestM (Lean.Server.RequestTask (Array Lean.Lsp.FoldingRange))

Equations

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

def Lean.Server.FileWorker.handleFoldingRange.isImport (stx : Lean.Syntax) : Bool

Equations

• Lean.Server.FileWorker.handleFoldingRange.isImport stx = (stx.isOfKind `Lean.Parser.Module.header || stx.isOfKind `Lean.Parser.Command.open)

partial def Lean.Server.FileWorker.handleFoldingRange.addRanges (text : Lean.FileMap) (sections : List (Nat × Option String.Pos)) : List Lean.Syntax → StateT (Array Lean.Lsp.FoldingRange) Lean.Server.RequestM PUnit

partial def Lean.Server.FileWorker.handleFoldingRange.addRanges.popRanges (text : Lean.FileMap) (stx : Lean.Syntax) (stxs : List Lean.Syntax) (n : Nat) (sections : List (Nat × Option String.Pos)) : StateT (Array Lean.Lsp.FoldingRange) Lean.Server.RequestM PUnit

def Lean.Server.FileWorker.handleFoldingRange.addCommandRange (text : Lean.FileMap) (stx : Lean.Syntax) : StateT (Array Lean.Lsp.FoldingRange) Lean.Server.RequestM PUnit

def Lean.Server.FileWorker.handleFoldingRange.addRangeFromSyntax (text : Lean.FileMap) (kind : Lean.Lsp.FoldingRangeKind) (stx : Lean.Syntax) : StateT (Array Lean.Lsp.FoldingRange) Lean.Server.RequestM PUnit

def Lean.Server.FileWorker.handleFoldingRange.addRange (text : Lean.FileMap) (kind : Lean.Lsp.FoldingRangeKind) (start? stop? : Option String.Pos) : StateT (Array Lean.Lsp.FoldingRange) Lean.Server.RequestM PUnit

Equations

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

def Lean.Server.FileWorker.handleWaitForDiagnostics (p : Lean.Lsp.WaitForDiagnosticsParams) : Lean.Server.RequestM (Lean.Server.RequestTask Lean.Lsp.WaitForDiagnostics)

partial def Lean.Server.FileWorker.handleWaitForDiagnostics.waitLoop (p : Lean.Lsp.WaitForDiagnosticsParams) : Lean.Server.RequestM Lean.Server.FileWorker.EditableDocument