def Lean.FileMap.rangeContainsHoverPos (text : FileMap) (r : Syntax.Range) (hoverPos : String.Pos.Raw) (includeStop : Bool := false) : Bool

Checks whether r contains hoverPos, taking into account EOF according to text.

def Lean.FileMap.rangeOverlapsRequestedRange (text : FileMap) (documentRange requestedRange : Syntax.Range) (includeDocumentRangeStop includeRequestedRangeStop : Bool := false) : Bool

def Lean.FileMap.rangeIncludesRequestedRange (text : FileMap) (documentRange requestedRange : Syntax.Range) (includeDocumentRangeStop includeRequestedRangeStop : Bool := false) : Bool

inductive Lean.Language.SnapshotTree.foldSnaps.Control : Type

• done : Control
• proceed (foldChildren : Bool) : Control

def Lean.Language.SnapshotTree.foldSnaps {α : Type u_1} (tree : SnapshotTree) (init : α) (f : SnapshotTask SnapshotTree → α → Server.ServerTask (α × foldSnaps.Control)) : Server.ServerTask α

def Lean.Language.SnapshotTree.findInfoTreeAtPos (text : FileMap) (tree : SnapshotTree) (hoverPos : String.Pos.Raw) (includeStop : Bool) : Server.ServerTask (Option Elab.InfoTree)

Finds the first (in pre-order) snapshot task in tree that contains hoverPos (including whitespace) and which contains an info tree, and then returns that info tree, waiting for any snapshot tasks on the way. Subtrees that do not contain the position are skipped without forcing their tasks. If the caller of this function needs the correct snapshot when the cursor is on whitespace, then this function is likely the wrong one to call, as it simply yields the first snapshot that contains hoverPos in its whitespace, which is not necessarily the correct one (e.g. it may be indentation-sensitive).

def Lean.Language.SnapshotTree.foldInfosInRange {α : Type u_1} (tree : SnapshotTree) (requestedRange : Syntax.Range) (init : α) (f : Elab.ContextInfo → Elab.Info → α → α) : Server.ServerTask α

def Lean.Language.SnapshotTree.collectMessagesInRange (tree : SnapshotTree) (requestedRange : Syntax.Range) : Server.ServerTask MessageLog

structure Lean.Server.RequestError : Type

• code : JsonRpc.ErrorCode
• message : String

@[implicit_reducible]

instance Lean.Server.instInhabitedRequestError : Inhabited RequestError

def Lean.Server.instInhabitedRequestError.default : RequestError

def Lean.Server.RequestError.fileChanged : RequestError

def Lean.Server.RequestError.methodNotFound (method : String) : RequestError

def Lean.Server.RequestError.invalidParams (message : String) : RequestError

def Lean.Server.RequestError.internalError (message : String) : RequestError

def Lean.Server.RequestError.requestCancelled : RequestError

def Lean.Server.RequestError.rpcNeedsReconnect : RequestError

def Lean.Server.RequestError.ofException (e : Exception) : IO RequestError

def Lean.Server.RequestError.ofIoError (e : IO.Error) : RequestError

def Lean.Server.RequestError.toLspResponseError (id : JsonRpc.RequestID) (e : RequestError) : JsonRpc.ResponseError Unit

def Lean.Server.parseRequestParams (paramType : Type) [FromJson paramType] (params : Json) : Except RequestError paramType

inductive Lean.Server.ServerRequestResponse (α : Type) : Type

• success {α : Type} (response : α) : ServerRequestResponse α
• failure {α : Type} (code : JsonRpc.ErrorCode) (message : String) : ServerRequestResponse α

@[implicit_reducible]

instance Lean.Server.instInhabitedServerRequestResponse {a✝ : Type} : Inhabited (ServerRequestResponse a✝)

def Lean.Server.instInhabitedServerRequestResponse.default {a✝ : Type} : ServerRequestResponse a✝

@[reducible, inline]

abbrev Lean.Server.ServerRequestEmitter : Type

structure Lean.Server.RequestContext : Type

• rpcSessions : Std.TreeMap UInt64 (IO.Ref FileWorker.RpcSession) compare
• doc : FileWorker.EditableDocument
• hLog : IO.FS.Stream
• initParams : Lsp.InitializeParams
• cancelTk : RequestCancellationToken
• serverRequestEmitter : ServerRequestEmitter

@[reducible, inline]

abbrev Lean.Server.RequestTask (α : Type u_1) : Type u_1

@[reducible, inline]

abbrev Lean.Server.RequestT (m : Type → Type u_1) (α : Type) : Type u_1

@[reducible, inline]

abbrev Lean.Server.RequestM (α : Type) : Type

Workers execute request handlers in this monad.

def Lean.Server.RequestM.run {α : Type} (act : RequestM α) (rc : RequestContext) : EIO RequestError α

@[reducible, inline]

abbrev Lean.Server.RequestTask.pure {α : Type u_1} (a : α) : RequestTask α

@[implicit_reducible]

instance Lean.Server.instMonadLiftIORequestM : MonadLift IO RequestM

@[implicit_reducible]

instance Lean.Server.instMonadLiftEIOExceptionRequestM : MonadLift (EIO Exception) RequestM

@[implicit_reducible]

instance Lean.Server.instMonadLiftCancellableMRequestM : MonadLift CancellableM RequestM

def Lean.Server.RequestM.runInIO {α : Type} (x : RequestM α) (ctx : RequestContext) : IO α

def Lean.Server.RequestM.readDoc {m : Type → Type u_1} [Monad m] [MonadReaderOf RequestContext m] : m FileWorker.EditableDocument

def Lean.Server.RequestM.asTask {α : Type} (t : RequestM α) : RequestM (RequestTask α)

def Lean.Server.RequestM.pureTask {α : Type} (t : RequestM α) : RequestM (RequestTask α)

def Lean.Server.RequestM.mapTaskCheap {α : Type u_1} {β : Type} (t : ServerTask α) (f : α → RequestM β) : RequestM (RequestTask β)

def Lean.Server.RequestM.mapTaskCostly {α : Type u_1} {β : Type} (t : ServerTask α) (f : α → RequestM β) : RequestM (RequestTask β)

def Lean.Server.RequestM.bindTaskCheap {α : Type u_1} {β : Type} (t : ServerTask α) (f : α → RequestM (RequestTask β)) : RequestM (RequestTask β)

def Lean.Server.RequestM.bindTaskCostly {α : Type u_1} {β : Type} (t : ServerTask α) (f : α → RequestM (RequestTask β)) : RequestM (RequestTask β)

def Lean.Server.RequestM.mapRequestTaskCheap {α : Type u_1} {β : Type} (t : RequestTask α) (f : α → RequestM β) : RequestM (RequestTask β)

def Lean.Server.RequestM.mapRequestTaskCostly {α : Type u_1} {β : Type} (t : RequestTask α) (f : α → RequestM β) : RequestM (RequestTask β)

def Lean.Server.RequestM.bindRequestTaskCheap {α : Type u_1} {β : Type} (t : RequestTask α) (f : α → RequestM (RequestTask β)) : RequestM (RequestTask β)

def Lean.Server.RequestM.bindRequestTaskCostly {α : Type u_1} {β : Type} (t : RequestTask α) (f : α → RequestM (RequestTask β)) : RequestM (RequestTask β)

def Lean.Server.RequestM.parseRequestParams (paramType : Type) [FromJson paramType] (params : Json) : RequestM paramType

def Lean.Server.RequestM.checkCancelled : RequestM Unit

def Lean.Server.RequestM.sendServerRequest (paramType : Type u_1) [ToJson paramType] (responseType : Type) [FromJson responseType] [Inhabited responseType] (method : String) (param : paramType) : RequestM (ServerTask (ServerRequestResponse responseType))

def Lean.Server.RequestM.waitFindSnapAux {α : Type} (notFoundX : RequestM α) (x : Snapshots.Snapshot → RequestM α) : Except IO.Error (Option Snapshots.Snapshot) → RequestM α

def Lean.Server.RequestM.withWaitFindSnap {β : Type} (doc : FileWorker.EditableDocument) (p : Snapshots.Snapshot → Bool) (notFoundX : RequestM β) (x : Snapshots.Snapshot → RequestM β) : RequestM (RequestTask β)

Create a task which waits for the first snapshot matching p, handles various errors, and if a matching snapshot was found executes x with it. If not found, the task executes notFoundX.

def Lean.Server.RequestM.bindWaitFindSnap {β : Type} (doc : FileWorker.EditableDocument) (p : Snapshots.Snapshot → Bool) (notFoundX : RequestM (RequestTask β)) (x : Snapshots.Snapshot → RequestM (RequestTask β)) : RequestM (RequestTask β)

See withWaitFindSnap.

def Lean.Server.RequestM.withWaitFindSnapAtPos {α : Type} (lspPos : Lsp.Position) (f : Snapshots.Snapshot → RequestM α) : RequestM (RequestTask α)

Create a task which waits for the snapshot containing lspPos and executes f with it. If no such snapshot exists, the request fails with an error.

def Lean.Server.RequestM.findCmdParsedSnap (doc : FileWorker.EditableDocument) (hoverPos : String.Pos.Raw) : ServerTask (Option Language.Lean.CommandParsedSnapshot)

Finds the first CommandParsedSnapshot containing hoverPos, asynchronously.

def Lean.Server.RequestM.findCmdDataAtPos (doc : FileWorker.EditableDocument) (hoverPos : String.Pos.Raw) (includeStop : Bool) : ServerTask (Option (Syntax × Elab.InfoTree))

Finds the command syntax and info tree of the first snapshot task containing pos, asynchronously. The info tree may be from a nested snapshot, such as a single tactic.

See SnapshotTree.findInfoTreeAtPos for details on how the search is done.

def Lean.Server.RequestM.findInfoTreeAtPos (doc : FileWorker.EditableDocument) (hoverPos : String.Pos.Raw) (includeStop : Bool) : ServerTask (Option Elab.InfoTree)

Finds the info tree of the first snapshot task containing pos, asynchronously. The info tree may be from a nested snapshot, such as a single tactic.

See SnapshotTree.findInfoTreeAtPos for details on how the search is done.

def Lean.Server.RequestM.runCommandElabM {α : Type} (snap : Snapshots.Snapshot) (c : RequestT Elab.Command.CommandElabM α) : RequestM α

def Lean.Server.RequestM.runCoreM {α : Type} (snap : Snapshots.Snapshot) (c : RequestT CoreM α) : RequestM α

def Lean.Server.RequestM.runTermElabM {α : Type} (snap : Snapshots.Snapshot) (c : RequestT Elab.TermElabM α) : RequestM α

The global request handlers table

We maintain a global map of LSP request handlers. This allows user code such as plugins to register its own handlers, for example to support ITP functionality such as goal state visualization.

For details of how to register one, see registerLspRequestHandler.

structure Lean.Server.LspResponse (α : Type) : Type

• response : α
• isComplete : Bool

structure Lean.Server.SerializedLspResponse : Type

• response? : Option Json
• serialized : String
• isComplete : Bool

def Lean.Server.SerializedLspResponse.toSerializedMessage (id : JsonRpc.RequestID) (r : SerializedLspResponse) : String

structure Lean.Server.RequestHandler : Type

• fileSource : Json → Except RequestError Lsp.DocumentUri
• handle : Json → RequestM (RequestTask SerializedLspResponse)

opaque Lean.Server.requestHandlers : IO.Ref (PersistentHashMap String RequestHandler)

def Lean.Server.registerLspRequestHandler (method : String) (paramType : Type) [FromJson paramType] [Lsp.FileSource paramType] (respType : Type) [ToJson respType] (handler : paramType → RequestM (RequestTask respType)) (serialize? : Option (respType → String) := none) : IO Unit

NB: This method may only be called in initialize blocks (user or builtin).

A registration consists of:

• a type of JSON-parsable request data paramType
• a FileSource instance for it so the system knows where to route requests
• a type of JSON-serializable response data respType
• an actual handler which runs in the RequestM monad and is expected to produce an asynchronous RequestTask which does any waiting/computation
• an optional serialize function which can be used to serialize respType directly to a string for performance reasons, skipping Json

A handler task may be cancelled at any time, so it should check the cancellation token when possible to handle this cooperatively. Any exceptions thrown in a request handler will be reported to the client as LSP error responses.

def Lean.Server.lookupLspRequestHandler (method : String) : IO (Option RequestHandler)

def Lean.Server.chainLspRequestHandler (method : String) (paramType : Type) [FromJson paramType] (respType : Type) [FromJson respType] [ToJson respType] (handler : paramType → RequestTask respType → RequestM (RequestTask respType)) : IO Unit

NB: This method may only be called in initialize blocks (user or builtin).

Register another handler to invoke after the last one registered for a method. At least one handler for the method must have already been registered to perform chaining.

For more details on the registration of a handler, see registerLspRequestHandler.

inductive Lean.Server.RequestHandlerCompleteness : Type

• complete : RequestHandlerCompleteness
• partial (refreshMethod : String) (refreshIntervalMs : Nat) : RequestHandlerCompleteness

  A request handler is partial if the LSP spec states that the request method implemented by the handler should be responded to with the full state of the document, but our implementation of the handler only returns a partial result for the document (e.g. only for the processed regions of the document, to reduce latency after a didChange). A request handler can only be partial if LSP also specifies a corresponding refresh server-to-client request, e.g. workspace/inlayHint/refresh for textDocument/inlayHint. This is necessary because we use the refresh request to prompt the client to re-request the data for a partial request if we returned a partial response for that request in the past, so that the client eventually converges to a complete set of information for the full document.

structure Lean.Server.StatefulRequestHandler : Type

• fileSource : Json → Except RequestError Lsp.DocumentUri
• pureHandle : Json → Dynamic → RequestM (SerializedLspResponse × Dynamic)

  handle with explicit state management for chaining request handlers. This function is pure w.r.t. lastTaskMutex and stateRef, but not RequestM.

• handle : Json → RequestM (RequestTask SerializedLspResponse)
• pureOnDidChange : Lsp.DidChangeTextDocumentParams → StateT Dynamic RequestM Unit

  onDidChange with explicit state management for chaining request handlers. This function is pure w.r.t. lastTaskMutex and stateRef, but not RequestM.

• onDidChange : Lsp.DidChangeTextDocumentParams → RequestM Unit
• lastTaskMutex : Std.Mutex (ServerTask Unit)
• initState : Dynamic
• stateRef : IO.Ref Dynamic

  stateRef is synchronized in registerStatefulLspRequestHandler by using lastTaskMutex to ensure that stateful request tasks for the same handler are executed sequentially (in order of arrival).

• completeness : RequestHandlerCompleteness

opaque Lean.Server.statefulRequestHandlers : IO.Ref (PersistentHashMap String StatefulRequestHandler)

def Lean.Server.registerCompleteStatefulLspRequestHandler (method : String) (paramType : Type) [FromJson paramType] [Lsp.FileSource paramType] (respType : Type) [ToJson respType] (stateType : Type) [TypeName stateType] (initState : stateType) (handler : paramType → stateType → RequestM (respType × stateType)) (onDidChange : Lsp.DidChangeTextDocumentParams → StateT stateType RequestM Unit) : IO Unit

def Lean.Server.registerPartialStatefulLspRequestHandler (method refreshMethod : String) (refreshIntervalMs : Nat) (paramType : Type) [FromJson paramType] [Lsp.FileSource paramType] (respType : Type) [ToJson respType] (stateType : Type) [TypeName stateType] (initState : stateType) (handler : paramType → stateType → RequestM (LspResponse respType × stateType)) (onDidChange : Lsp.DidChangeTextDocumentParams → StateT stateType RequestM Unit) : IO Unit

def Lean.Server.isStatefulLspRequestMethod (method : String) : BaseIO Bool

def Lean.Server.lookupStatefulLspRequestHandler (method : String) : BaseIO (Option StatefulRequestHandler)

def Lean.Server.partialLspRequestHandlerMethods : IO (Array (String × String × Nat))

def Lean.Server.chainStatefulLspRequestHandler (method : String) (paramType : Type) [FromJson paramType] [ToJson paramType] [Lsp.FileSource paramType] (respType : Type) [FromJson respType] [ToJson respType] (stateType : Type) [TypeName stateType] (handler : paramType → LspResponse respType → stateType → RequestM (LspResponse respType × stateType)) (onDidChange : Lsp.DidChangeTextDocumentParams → StateT stateType RequestM Unit) : IO Unit

def Lean.Server.handleOnDidChange (p : Lsp.DidChangeTextDocumentParams) : RequestM Unit

def Lean.Server.handleLspRequest (method : String) (params : Json) : RequestM (RequestTask SerializedLspResponse)

def Lean.Server.routeLspRequest (method : String) (params : Json) : IO (Except RequestError Lsp.DocumentUri)