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

Equations

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

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.

Equations

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

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? : optParam (Option Lean.Elab.InfoTree) none) : Lean.Server.RequestM (Array Lean.Lsp.LocationLink)

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Server.FileWorker.locationLinksOfInfo.extractInstances i ci x = pure #[]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

structure Lean.Server.FileWorker.SemanticTokensContext : Type

• beginPos : String.Pos
• endPos : String.Pos
• text : Lean.FileMap
• snap : Lean.Server.Snapshots.Snapshot

structure Lean.Server.FileWorker.SemanticTokensState : Type

• data : Array Nat
• lastLspPos : Lean.Lsp.Position

def Lean.Server.FileWorker.keywordSemanticTokenMap : Lean.RBMap String Lean.Lsp.SemanticTokenType compare

Equations

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

def Lean.Server.FileWorker.handleSemanticTokens (beginPos : String.Pos) (endPos : String.Pos) : Lean.Server.RequestM (Lean.Server.RequestTask Lean.Lsp.SemanticTokens)

Equations

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

partial def Lean.Server.FileWorker.handleSemanticTokens.go (stx : Lean.Syntax) : ReaderT Lean.Server.FileWorker.SemanticTokensContext (StateT Lean.Server.FileWorker.SemanticTokensState Lean.Server.RequestM) PUnit

def Lean.Server.FileWorker.handleSemanticTokens.highlightId (stx : Lean.Syntax) : ReaderT Lean.Server.FileWorker.SemanticTokensContext (StateT Lean.Server.FileWorker.SemanticTokensState Lean.Server.RequestM) PUnit

Equations

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

def Lean.Server.FileWorker.handleSemanticTokens.highlightKeyword (stx : Lean.Syntax) : ReaderT Lean.Server.FileWorker.SemanticTokensContext (StateT Lean.Server.FileWorker.SemanticTokensState Lean.Server.RequestM) PUnit

Equations

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

def Lean.Server.FileWorker.handleSemanticTokens.addToken (stx : Lean.Syntax) (type : Lean.Lsp.SemanticTokenType) : ReaderT Lean.Server.FileWorker.SemanticTokensContext (StateT Lean.Server.FileWorker.SemanticTokensState Lean.Server.RequestM) PUnit

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)

Equations

• Lean.Server.FileWorker.handleSemanticTokensFull x = Lean.Server.FileWorker.handleSemanticTokens 0 { byteIdx := 1 <<< 31 }

def Lean.Server.FileWorker.handleSemanticTokensRange (p : Lean.Lsp.SemanticTokensRangeParams) : Lean.Server.RequestM (Lean.Server.RequestTask Lean.Lsp.SemanticTokens)

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 = (Lean.Syntax.isOfKind stx `Lean.Parser.Module.header || Lean.Syntax.isOfKind stx `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

Equations

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

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

Equations

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

def Lean.Server.FileWorker.handleFoldingRange.addRange (text : Lean.FileMap) (kind : Lean.Lsp.FoldingRangeKind) (start? : Option String.Pos) (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)

Equations

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

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