partial def Lean.Language.SnapshotTree.findInfoTreeAtPos (tree : SnapshotTree) (pos : String.Pos) : Task (Option Elab.InfoTree)

Finds the first (in pre-order) snapshot task in tree whose range? contains pos 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.

partial def Lean.Language.SnapshotTree.findInfoTreeAtPos.goSeq (pos : String.Pos) : List (SnapshotTask SnapshotTree) → Task (Option Elab.InfoTree)

structure Lean.Server.RequestError : Type

• code : JsonRpc.ErrorCode
• message : String

instance Lean.Server.instInhabitedRequestError : Inhabited RequestError

Equations

• Lean.Server.instInhabitedRequestError = { default := { code := default, message := default } }

def Lean.Server.RequestError.fileChanged : RequestError

Equations

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

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

Equations

• Lean.Server.RequestError.methodNotFound method = { code := Lean.JsonRpc.ErrorCode.methodNotFound, message := toString "No request handler found for '" ++ toString method ++ toString "'" }

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

Equations

• Lean.Server.RequestError.invalidParams message = { code := Lean.JsonRpc.ErrorCode.invalidParams, message := message }

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

Equations

• Lean.Server.RequestError.internalError message = { code := Lean.JsonRpc.ErrorCode.internalError, message := message }

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

Equations

• Lean.Server.RequestError.ofException e = do let __do_lift ← liftM e.toMessageData.toString pure (Lean.Server.RequestError.internalError __do_lift)

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

Equations

• Lean.Server.RequestError.ofIoError e = Lean.Server.RequestError.internalError (toString e)

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

Equations

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

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

Equations

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

structure Lean.Server.RequestContext : Type

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

• Lean.Server.RequestT m = ReaderT Lean.Server.RequestContext (ExceptT Lean.Server.RequestError m)

@[reducible, 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)

@[reducible, inline]

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

Equations

• Lean.Server.RequestTask.pure a = { get := Except.ok a }

instance Lean.Server.instMonadLiftIORequestM : MonadLift IO RequestM

Equations

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

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

Equations

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

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

Equations

• Lean.Server.RequestM.readDoc = do let rc ← readThe Lean.Server.RequestContext pure rc.doc

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

Equations

• t.asTask = do let rc ← readThe Lean.Server.RequestContext liftM (ReaderT.run t rc).asTask

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

Equations

• Lean.Server.RequestM.mapTask t f = do let rc ← readThe Lean.Server.RequestContext liftM (EIO.mapTask (fun (x : α) => f x rc) t)

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

Equations

• Lean.Server.RequestM.bindTask t f = do let rc ← readThe Lean.Server.RequestContext liftM (EIO.bindTask t fun (x : α) => f x rc)

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

Equations

• notFoundX.waitFindSnapAux x (Except.error e) = throw (Lean.Server.RequestError.ofIoError e)
• notFoundX.waitFindSnapAux x (Except.ok none) = notFoundX
• notFoundX.waitFindSnapAux x (Except.ok (some snap)) = x snap

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.

Equations

• Lean.Server.RequestM.withWaitFindSnap doc p notFoundX x = Lean.Server.RequestM.mapTask (IO.AsyncList.waitFind? p doc.cmdSnaps) (notFoundX.waitFindSnapAux x)

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.

Equations

• Lean.Server.RequestM.bindWaitFindSnap doc p notFoundX x = Lean.Server.RequestM.bindTask (IO.AsyncList.waitFind? p doc.cmdSnaps) (notFoundX.waitFindSnapAux x)

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.

Equations

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

def Lean.Server.RequestM.findCmdParsedSnap (doc : FileWorker.EditableDocument) (p : Language.Lean.CommandParsedSnapshot → Bool) : Task (Option Language.Lean.CommandParsedSnapshot)

Finds the first CommandParsedSnapshot fulfilling p, asynchronously.

Equations

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

partial def Lean.Server.RequestM.findCmdParsedSnap.go (p : Language.Lean.CommandParsedSnapshot → Bool) (cmdParsed : Language.Lean.CommandParsedSnapshot) : Task (Option Language.Lean.CommandParsedSnapshot)

def Lean.Server.RequestM.findInfoTreeAtPos (doc : FileWorker.EditableDocument) (isMatchingSnapshot : Language.Lean.CommandParsedSnapshot → Bool) (pos : String.Pos) : Task (Option Elab.InfoTree)

Finds the info tree of the first snapshot task matching isMatchingSnapshot and 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.

Equations

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

def Lean.Server.RequestM.findCmdDataAtPos (doc : FileWorker.EditableDocument) (isMatchingSnapshot : Language.Lean.CommandParsedSnapshot → Bool) (pos : String.Pos) : Task (Option (Syntax × Elab.InfoTree))

Finds the command syntax and info tree of the first snapshot task matching isMatchingSnapshot and 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.

Equations

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

def Lean.Server.RequestM.findInfoTreeAtPosWithTrailingWhitespace (doc : FileWorker.EditableDocument) (pos : String.Pos) : Task (Option Elab.InfoTree)

Finds the info tree of the first snapshot task containing pos (including trailing whitespace), 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.

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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 : Json → Except RequestError Lsp.DocumentUri
• handle : Json → RequestM (RequestTask Json)

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

Equations

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

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

Equations

• Lean.Server.lookupLspRequestHandler method = do let __do_lift ← ST.Ref.get Lean.Server.requestHandlers pure (__do_lift.find? method)

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.

Equations

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

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

Equations

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

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

Equations

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