From f4dbd4d3e80432cf1bd41d7f423580da153f11b8 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 16 Apr 2013 10:55:48 -0400 Subject: Basis.tryRpc --- doc/manual.tex | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'doc/manual.tex') diff --git a/doc/manual.tex b/doc/manual.tex index a402c6b6..0af87d8e 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -2157,6 +2157,12 @@ $$\begin{array}{l} \mt{val} \; \mt{rpc} : \mt{t} ::: \mt{Type} \to \mt{transaction} \; \mt{t} \to \mt{transaction} \; \mt{t} \end{array}$$ +There is an alternate form that uses $\mt{None}$ to indicate that an error occurred during RPC processing, rather than raising an exception to abort this branch of control flow. + +$$\begin{array}{l} + \mt{val} \; \mt{tryRpc} : \mt{t} ::: \mt{Type} \to \mt{transaction} \; \mt{t} \to \mt{transaction} \; (\mt{option} \; \mt{t}) +\end{array}$$ + \subsubsection{Asynchronous Message-Passing} To support asynchronous, ``server push'' delivery of messages to clients, any client that might need to receive an asynchronous message is assigned a unique ID. These IDs may be retrieved both on the client and on the server, during execution of code related to a client. -- cgit v1.2.3