diff doc/manual.tex @ 1848:e15234fbb163

Basis.tryRpc
author Adam Chlipala <adam@chlipala.net>
date Tue, 16 Apr 2013 10:55:48 -0400
parents 2c5e6f78560c
children 30c56e3bcf47
line wrap: on
line diff
--- a/doc/manual.tex	Mon Apr 01 10:13:49 2013 -0400
+++ b/doc/manual.tex	Tue Apr 16 10:55:48 2013 -0400
@@ -2157,6 +2157,12 @@
   \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.