equal
deleted
inserted
replaced
200 if is_protocol_exn exn then Exn.reraise exn |
200 if is_protocol_exn exn then Exn.reraise exn |
201 else (Runtime.exn_system_message exn handle crash => recover crash); |
201 else (Runtime.exn_system_message exn handle crash => recover crash); |
202 in protocol_loop () end; |
202 in protocol_loop () end; |
203 |
203 |
204 fun protocol () = |
204 fun protocol () = |
205 (ml_statistics (); |
205 (message Markup.initN [] [XML.Text (Session.welcome ())]; |
206 message Markup.initN [] [XML.Text (Session.welcome ())]; |
206 ml_statistics (); |
207 protocol_loop ()); |
207 protocol_loop ()); |
208 |
208 |
209 val result = Exn.capture (message_context protocol) (); |
209 val result = Exn.capture (message_context protocol) (); |
210 |
210 |
211 |
211 |