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.handleDefinition (kind : GoToKind) (p : Lsp.TextDocumentPositionParams) : RequestM (RequestTask (Array Lsp.LeanLocationLink))

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

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.

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.handleSignatureHelp (p : Lsp.SignatureHelpParams) : RequestM (RequestTask (Option Lsp.SignatureHelp))

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.