comparison 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
comparison
equal deleted inserted replaced
1847:8958b580d026 1848:e15234fbb163
2153 2153
2154 Any function call may be made a client-to-server ``remote procedure call'' if the function being called needs no features that are only available to client code. To make a function call an RPC, pass that function call as the argument to $\mt{Basis.rpc}$: 2154 Any function call may be made a client-to-server ``remote procedure call'' if the function being called needs no features that are only available to client code. To make a function call an RPC, pass that function call as the argument to $\mt{Basis.rpc}$:
2155 2155
2156 $$\begin{array}{l} 2156 $$\begin{array}{l}
2157 \mt{val} \; \mt{rpc} : \mt{t} ::: \mt{Type} \to \mt{transaction} \; \mt{t} \to \mt{transaction} \; \mt{t} 2157 \mt{val} \; \mt{rpc} : \mt{t} ::: \mt{Type} \to \mt{transaction} \; \mt{t} \to \mt{transaction} \; \mt{t}
2158 \end{array}$$
2159
2160 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.
2161
2162 $$\begin{array}{l}
2163 \mt{val} \; \mt{tryRpc} : \mt{t} ::: \mt{Type} \to \mt{transaction} \; \mt{t} \to \mt{transaction} \; (\mt{option} \; \mt{t})
2158 \end{array}$$ 2164 \end{array}$$
2159 2165
2160 \subsubsection{Asynchronous Message-Passing} 2166 \subsubsection{Asynchronous Message-Passing}
2161 2167
2162 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. 2168 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.