Lean.Server.Requests

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.

source

structure Lean.Server.RequestError:

Type

code : Lean.JsonRpc.ErrorCode
message : String

source

def Lean.Server.RequestError.fileChanged:

Lean.Server.RequestError

Equations

Lean.Server.RequestError.fileChanged = { code := Lean.JsonRpc.ErrorCode.contentModified, message := "File changed." }

source

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

Lean.Server.RequestError

Equations

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

source

instance Lean.Server.RequestError.instCoeErrorRequestError:

Coe IO.Error Lean.Server.RequestError

Equations

Lean.Server.RequestError.instCoeErrorRequestError = { coe := fun e => { code := Lean.JsonRpc.ErrorCode.internalError, message := toString e } }

source

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

Lean.JsonRpc.ResponseError Unit

Equations

Lean.Server.RequestError.toLspResponseError id e = { id := id, code := e.code, message := e.message, data? := none }

source

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

Except Lean.Server.RequestError paramType

Equations

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

source

structure Lean.Server.RequestContext:

Type

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

source

@[inline]

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

Type u_1

Equations

Lean.Server.RequestTask α = Task (Except Lean.Server.RequestError α)

source

@[inline]

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

Type

Workers execute request handlers in this monad.

Equations

Lean.Server.RequestM = ReaderT Lean.Server.RequestContext (EIO Lean.Server.RequestError)

source

instance Lean.Server.instInhabitedRequestM {α : Type} :

Inhabited (Lean.Server.RequestM α)

Equations

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

source

instance Lean.Server.instMonadLiftIORequestM:

MonadLift IO Lean.Server.RequestM

Equations

Lean.Server.instMonadLiftIORequestM = { monadLift := fun {α} x => liftM (IO.toEIO (fun e => { code := Lean.JsonRpc.ErrorCode.internalError, message := toString e }) x) }

source

def Lean.Server.RequestM.readDoc:

Lean.Server.RequestM Lean.Server.FileWorker.EditableDocument

Equations

Lean.Server.RequestM.readDoc rc = pure rc.doc

source

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

Lean.Server.RequestM (Lean.Server.RequestTask α)

Equations

Lean.Server.RequestM.asTask t rc = do let t ← liftM (EIO.asTask (t rc) Task.Priority.default) pure (Task.map liftExcept t)

source

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

Lean.Server.RequestM (Lean.Server.RequestTask β)

Equations

Lean.Server.RequestM.mapTask t f rc = do let t ← liftM (EIO.mapTask (fun a => f a rc) t Task.Priority.default) pure (Task.map liftExcept t)

source

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

Lean.Server.RequestM (Lean.Server.RequestTask β)

Equations

Lean.Server.RequestM.bindTask t f rc = liftM (EIO.bindTask t (fun a => f a rc) Task.Priority.default)

source

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

Except Lean.Server.FileWorker.ElabTaskError (Option Lean.Server.Snapshots.Snapshot) → Lean.Server.RequestM α

Equations

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

source

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

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.

Equations

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

source

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

Lean.Server.RequestM (Lean.Server.RequestTask β)

See withWaitFindSnap.

Equations

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

source

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)

source

opaque Lean.Server.requestHandlers:

IO.Ref (Std.PersistentHashMap String Lean.Server.RequestHandler)

source

def Lean.Server.registerLspRequestHandler (method : String) (paramType : Type) [inst : Lean.FromJson paramType] [inst : Lean.Lsp.FileSource paramType] (respType : Type) [inst : Lean.ToJson respType] (handler : paramType → Lean.Server.RequestM (Lean.Server.RequestTask respType)) :

IO Unit

NB: This method may only be called in builtin_initialize blocks.

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.

Equations

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

source

def Lean.Server.lookupLspRequestHandler (method : String) :

IO (Option Lean.Server.RequestHandler)

Equations

Lean.Server.lookupLspRequestHandler method = do let a ← ST.Ref.get Lean.Server.requestHandlers pure (Std.PersistentHashMap.find? a method)

source

def Lean.Server.chainLspRequestHandler (method : String) (paramType : Type) [inst : Lean.FromJson paramType] (respType : Type) [inst : Lean.FromJson respType] [inst : 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 builtin_initialize blocks.

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.

Equations

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

source

def Lean.Server.routeLspRequest (method : String) (params : Lean.Json) :

IO (Except Lean.Server.RequestError Lean.Lsp.DocumentUri)

Equations

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

source

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

Lean.Server.RequestM (Lean.Server.RequestTask Lean.Json)

Equations

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