Documentation

ProofWidgets.Cancellable

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.

@[inline, reducible]
Equations
Instances For

    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.

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

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

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

        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.

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