3 files changed, 14 insertions, 22 deletions
diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index 9f496f5845..3dc0597101 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -66,12 +66,10 @@ let print_anomaly askreport e =
 
 let handle_stack = ref []
 
-exception Unhandled
-
 let register_handler h = handle_stack := h::!handle_stack
 
 let is_handled e =
-  let is_handled_by h = (try let _ = h e in true with | Unhandled -> false) in
+  let is_handled_by h = Option.has_some (h e) in
   List.exists is_handled_by !handle_stack
 
 let is_anomaly = function
@@ -93,12 +91,11 @@ let rec print_gen ~anomaly ~extra_msg stk (e, info) =
   | [] ->
     print_anomaly anomaly e
   | h::stk' ->
-    try
-      let err_msg = h e in
+    match h e with
+    | Some err_msg ->
       Option.cata (fun msg -> msg ++ err_msg) err_msg extra_msg
-    with
-    | Unhandled -> print_gen ~anomaly ~extra_msg stk' (e,info)
-    | any -> print_gen ~anomaly ~extra_msg stk' (any,info)
+    | None ->
+      print_gen ~anomaly ~extra_msg stk' (e,info)
 
 let print_gen ~anomaly (e, info) =
   let extra_info =
@@ -130,8 +127,8 @@ let print_no_report e = iprint_no_report (e, Exninfo.info e)
 
 let _ = register_handler begin function
   | UserError(s, pps) ->
-    where s ++ pps
-  | _ -> raise Unhandled
+    Some (where s ++ pps)
+  | _ -> None
 end
 
 (** Critical exceptions should not be caught and ignored by mistake
diff --git a/lib/cErrors.mli b/lib/cErrors.mli
index 02eaf6bd0b..1660a00244 100644
--- a/lib/cErrors.mli
+++ b/lib/cErrors.mli
@@ -46,19 +46,14 @@ exception Timeout
     recent first) until a handle deals with it.
 
     Handles signal that they don't deal with some exception
-    by raising [Unhandled].
+    by returning None. Raising any other exception is
+    forbidden and will result in an anomaly.
 
-    Handles can raise exceptions themselves, in which
-    case, the exception is passed to the handles which
-    were registered before.
-
-    The exception that are considered anomalies should not be
+    Exceptions that are considered anomalies should not be
     handled by registered handlers.
 *)
 
-exception Unhandled
-
-val register_handler : (exn -> Pp.t) -> unit
+val register_handler : (exn -> Pp.t option) -> unit
 
 (** The standard exception printer *)
 val print : exn -> Pp.t
diff --git a/lib/future.ml b/lib/future.ml
index 5cccd2038d..ddf841b7fc 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -28,9 +28,9 @@ exception NotReady of string
 exception NotHere of string
 
 let _ = CErrors.register_handler (function
-  | NotReady name -> !not_ready_msg name
-  | NotHere name -> !not_here_msg name
-  | _ -> raise CErrors.Unhandled)
+  | NotReady name -> Some (!not_ready_msg name)
+  | NotHere name -> Some (!not_here_msg name)
+  | _ -> None)
 
 type fix_exn = Exninfo.iexn -> Exninfo.iexn
 let id x = x