structure Lean.Server.RequestError : Type

• code : Lean.JsonRpc.ErrorCode
• message : String

instance Lean.Server.instInhabitedRequestError : Inhabited Lean.Server.RequestError

def Lean.Server.RequestError.fileChanged : Lean.Server.RequestError

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

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

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

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

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

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

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

structure Lean.Server.RequestContext : Type

• rpcSessions : Lean.RBMap UInt64 (IO.Ref Lean.Server.FileWorker.RpcSession) compare
• srcSearchPath : Lean.SearchPath
• doc : Lean.Server.FileWorker.EditableDocument
• hLog : IO.FS.Stream
• hOut : IO.FS.Stream
• initParams : Lean.Lsp.InitializeParams

@[inline, reducible]

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

@[inline, reducible]

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

@[inline, reducible]

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

Workers execute request handlers in this monad.

@[inline, reducible]

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

instance Lean.Server.instMonadLiftIORequestM : MonadLift IO Lean.Server.RequestM

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

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

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

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

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

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

def Lean.Server.RequestM.withWaitFindSnap {β : Type} (doc : Lean.Server.FileWorker.EditableDocument) (p : Lean.Server.Snapshots.Snapshot → Bool) (notFoundX : Lean.Server.RequestM β) (x : Lean.Server.Snapshots.Snapshot → Lean.Server.RequestM β) (abortedX : optParam (Lean.Server.RequestM β) (throwThe Lean.Server.RequestError Lean.Server.RequestError.fileChanged)) : Lean.Server.RequestM (Lean.Server.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 : Lean.Server.FileWorker.EditableDocument) (p : Lean.Server.Snapshots.Snapshot → Bool) (notFoundX : Lean.Server.RequestM (Lean.Server.RequestTask β)) (x : Lean.Server.Snapshots.Snapshot → Lean.Server.RequestM (Lean.Server.RequestTask β)) (abortedX : optParam (Lean.Server.RequestM (Lean.Server.RequestTask β)) (throwThe Lean.Server.RequestError Lean.Server.RequestError.fileChanged)) : Lean.Server.RequestM (Lean.Server.RequestTask β)

See withWaitFindSnap.

def Lean.Server.RequestM.withWaitFindSnapAtPos {α : Type} (lspPos : Lean.Lsp.Position) (f : Lean.Server.Snapshots.Snapshot → Lean.Server.RequestM α) : Lean.Server.RequestM (Lean.Server.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.runCommandElabM {α : Type} (snap : Lean.Server.Snapshots.Snapshot) (c : Lean.Server.RequestT Lean.Elab.Command.CommandElabM α) : Lean.Server.RequestM α

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

def Lean.Server.RequestM.runTermElabM {α : Type} (snap : Lean.Server.Snapshots.Snapshot) (c : Lean.Server.RequestT Lean.Elab.TermElabM α) : Lean.Server.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.RequestHandler : Type

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

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

def Lean.Server.registerLspRequestHandler (method : String) (paramType : Type) [Lean.FromJson paramType] [Lean.Lsp.FileSource paramType] (respType : Type) [Lean.ToJson respType] (handler : paramType → Lean.Server.RequestM (Lean.Server.RequestTask respType)) : 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

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 Lean.Server.RequestHandler)

def Lean.Server.chainLspRequestHandler (method : String) (paramType : Type) [Lean.FromJson paramType] (respType : Type) [Lean.FromJson respType] [Lean.ToJson respType] (handler : paramType → Lean.Server.RequestTask respType → Lean.Server.RequestM (Lean.Server.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.

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

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