Experimental support for cancellable RPC requests.

Note: Cancellation should eventually become a feature of the core RPC protocol, and the requests map should be stored in RequestM, or somewhere in the server anyway.

@[reducible, inline]

abbrev ProofWidgets.RequestId : Type

structure ProofWidgets.CancellableTask : Type

• task : Task (Except Lean.Server.RequestError (LazyEncodable Lean.Json))
• cancel : IO Unit

opaque ProofWidgets.runningRequests : IO.Ref (RequestId × Std.HashMap RequestId CancellableTask)

Maps the ID of each currently executing request to its task.

def ProofWidgets.mkCancellable {β : Type} {α : Sort u_1} [Lean.Server.RpcEncodable β] (handler : α → Lean.Server.RequestM (Lean.Server.RequestTask β)) : α → Lean.Server.RequestM (Lean.Server.RequestTask RequestId)

Transforms a request handler returning β into one that returns immediately with a RequestId.

The ID uniquely identifies the running request: its results can be retrieved using checkRequest, and it can be cancelled using cancelRequest.

def ProofWidgets.cancelRequest (rid : RequestId) : Lean.Server.RequestM (Lean.Server.RequestTask String)

Cancel the request with ID rid. Does nothing if rid is invalid.

inductive ProofWidgets.CheckRequestResponse : Type

The status of a running cancellable request.

• running : CheckRequestResponse
• done (result : LazyEncodable Lean.Json) : CheckRequestResponse

instance ProofWidgets.instRpcEncodableCheckRequestResponse : Lean.Server.RpcEncodable CheckRequestResponse

def ProofWidgets.checkRequest (rid : RequestId) : Lean.Server.RequestM (Lean.Server.RequestTask CheckRequestResponse)

Check whether a request has finished computing, and return the response if so. The request is removed from runningRequests the first time it is checked and found to have finished. Throws an error if the rid is invalid, or if the request itself threw an error.

def ProofWidgets.cancellableSuffix : Lean.Name