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

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

Instances For

source
def Lean.Server.FileWorker.handleCompletion (p : Lsp.CompletionParams) :
RequestM (RequestTask Lsp.ResolvableCompletionList)
Equations

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
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

Instances For

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

Instances For

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

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
def Lean.Server.FileWorker.handleDocumentColor :
Lsp.DocumentColorParams → RequestM (RequestTask (Array Lsp.ColorInformation))
Equations

- Lean.Server.FileWorker.handleDocumentColor x✝ = pure (Lean.Server.RequestTask.pure #[])

Instances For