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.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) (ci : Lean.Elab.ContextInfo) (i : Lean.Elab.Info) (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.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

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) : List Lean.Lsp.DocumentSymbol × List Lean.Syntax

partial def Lean.Server.FileWorker.handleDocumentSymbol.sectionLikeToDocumentSymbols (text : Lean.FileMap) (stx : Lean.Syntax) (stxs : List Lean.Syntax) (name : String) (kind : Lean.Lsp.SymbolKind) (selection : Lean.Syntax) : List Lean.Lsp.DocumentSymbol × List Lean.Syntax

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

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

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

partial def Lean.Server.FileWorker.handleFoldingRange.addRanges (text : Lean.FileMap) (sections : List (Option String.Pos)) : List Lean.Syntax → 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