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

Equations

• Lean.Server.FileWorker.findCompletionCmdDataAtPos doc pos = Lean.Server.RequestM.findCmdDataAtPos doc pos true

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

Equations

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

def Lean.Server.FileWorker.handleCompletionItemResolve (item : Lsp.CompletionItem) : RequestM (RequestTask 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.

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Server.FileWorker.locationLinksOfInfo.extractInstances i ci (Lean.Expr.mdata data e) = Lean.Server.FileWorker.locationLinksOfInfo.extractInstances i ci e
• Lean.Server.FileWorker.locationLinksOfInfo.extractInstances i ci x✝ = pure #[]

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

Equations

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

def Lean.Server.FileWorker.findGoalsAt? (doc : EditableDocument) (hoverPos : String.Pos) : ServerTask (Option (List Elab.GoalsAtResult))

Equations

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

def Lean.Server.FileWorker.findGoalsAt?.getPositions (snap : Language.SnapshotTask Language.SnapshotTree) : Option (String.Pos × String.Pos × String.Pos)

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

structure Lean.Server.FileWorker.NamespaceEntry : Type

• name : List 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 : Syntax
• selection : Syntax
• prevSiblings : Array Lsp.DocumentSymbol

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

Equations

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

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

Equations

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

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

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

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

Equations

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

def Lean.Server.FileWorker.handleFoldingRange.isImport (stx : 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 : FileMap) (sections : List (Nat × Option String.Pos)) : List Syntax → StateT (Array Lsp.FoldingRange) RequestM PUnit

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

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

Equations

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

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

Equations

• Lean.Server.FileWorker.handleFoldingRange.addRangeFromSyntax text kind stx = Lean.Server.FileWorker.handleFoldingRange.addRange text kind stx.getPos? stx.getTailPos?

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

Equations

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

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

Equations

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

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