Documentation

Lean.Server.FileWorker.RequestHandling

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

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

Lean.Server.FileWorker.noHighlightKinds = #[`Lean.Parser.Term.sorry, `Lean.Parser.Term.type, `Lean.Parser.Term.prop, `antiquotName, `Lean.Parser.Command.docComment]

structure Lean.Server.FileWorker.SemanticTokensContext:

Type

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

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