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

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

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)

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

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

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

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

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

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

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

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

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

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

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

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

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

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? : Option String.Pos) (stop? : Option String.Pos) : StateT (Array Lean.Lsp.FoldingRange) Lean.Server.RequestM PUnit

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