From c216daf5d5f8215947bce10e55d30c35be1a56ba Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 31 Jan 2020 15:57:45 +0100
Subject: [exn] Forbid raising in exn printers, make them return Pp.t option

Raising inside exception printers is quite tricky as the order of
registration for printers will indeed depend on the linking order.

We thus forbid this, and make our API closer to the upstream
`Printexn` by having printers return an option type.
---
 stm/stm.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index a521f9001d..c79a1eed3d 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1273,8 +1273,8 @@ let record_pb_time ?loc proof_name time =
 
 exception RemoteException of Pp.t
 let _ = CErrors.register_handler (function
-  | RemoteException ppcmd -> ppcmd
-  | _ -> raise Unhandled)
+  | RemoteException ppcmd -> Some ppcmd
+  | _ -> None)
 
 (****************** proof structure for error recovery ************************)
 (******************************************************************************)
-- 
cgit v1.2.3