[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.

16 files changed, 73 insertions, 67 deletions

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 42dd2dd052..d5938713d6 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -15,6 +15,12 @@ Exception handling:
   `Exninfo.capture` and `iraise` when re-raising inside an exception
   handler.
 
+- Registration of exception printers now follows more closely OCaml's
+  API, thus:
+
+  + printers are of type `exn -> Pp.t option` [`None` == not handled]
+  + it is forbidden for exception printers to raise.
+
 Printers:
 
 - Functions such as Printer.pr_lconstr_goal_style_env have been
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 3c383b2e00..605877cfba 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -38,9 +38,9 @@ exception Tac_Timeout
 exception TacticFailure of exn
 
 let _ = CErrors.register_handler begin function
-  | Exception e -> CErrors.print e
-  | TacticFailure e -> CErrors.print e
-  | _ -> raise CErrors.Unhandled
+  | Exception e -> Some (CErrors.print e)
+  | TacticFailure e -> Some (CErrors.print e)
+  | _ -> None
 end
 
 (** {6 Non-logical layer} *)
diff --git a/engine/proofview.ml b/engine/proofview.ml
index b0ea75ac60..31e4dae2de 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -303,8 +303,8 @@ let tclONCE = Proof.once
 exception MoreThanOneSuccess
 let _ = CErrors.register_handler begin function
   | MoreThanOneSuccess ->
-    Pp.str "This tactic has more than one success."
-  | _ -> raise CErrors.Unhandled
+    Some (Pp.str "This tactic has more than one success.")
+  | _ -> None
 end
 
 (** [tclEXACTLY_ONCE e t] succeeds as [t] if [t] has exactly one
@@ -348,8 +348,8 @@ exception NoSuchGoals of int
 
 let _ = CErrors.register_handler begin function
   | NoSuchGoals n ->
-    str "No such " ++ str (String.plural n "goal") ++ str "."
-  | _ -> raise CErrors.Unhandled
+    Some (str "No such " ++ str (String.plural n "goal") ++ str ".")
+  | _ -> None
 end
 
 (** [tclFOCUS ?nosuchgoal i j t] applies [t] in a context where
@@ -421,9 +421,10 @@ exception SizeMismatch of int*int
 let _ = CErrors.register_handler begin function
   | SizeMismatch (i,j) ->
     let open Pp in
-    str"Incorrect number of goals" ++ spc() ++
-    str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str")."
-  | _ -> raise CErrors.Unhandled
+    Some (
+      str"Incorrect number of goals" ++ spc() ++
+      str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str").")
+  | _ -> None
 end
 
 (** A variant of [Monad.List.iter] where we iter over the focused list
@@ -908,8 +909,8 @@ let tclPROGRESS t =
 
 let _ = CErrors.register_handler begin function
   | Logic_monad.Tac_Timeout ->
-    Pp.str "[Proofview.tclTIMEOUT] Tactic timeout!"
-  | _ -> raise CErrors.Unhandled
+    Some (Pp.str "[Proofview.tclTIMEOUT] Tactic timeout!")
+  | _ -> None
 end
 
 let tclTIMEOUT n t =
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
diff --git a/proofs/proof.ml b/proofs/proof.ml
index e2ee5426b5..7d0b31734e 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -69,16 +69,16 @@ exception FullyUnfocused
 
 let _ = CErrors.register_handler begin function
   | CannotUnfocusThisWay ->
-    Pp.str "This proof is focused, but cannot be unfocused this way"
+    Some (Pp.str "This proof is focused, but cannot be unfocused this way")
   | NoSuchGoals (i,j) when Int.equal i j ->
-    Pp.(str "[Focus] No such goal (" ++ int i ++ str").")
+    Some Pp.(str "[Focus] No such goal (" ++ int i ++ str").")
   | NoSuchGoals (i,j) ->
-    Pp.(str "[Focus] Not every goal in range ["++ int i ++ str","++int j++str"] exist.")
+    Some Pp.(str "[Focus] Not every goal in range ["++ int i ++ str","++int j++str"] exist.")
   | NoSuchGoal id ->
-    Pp.(str "[Focus] No such goal: " ++ str (Names.Id.to_string id) ++ str ".")
+    Some Pp.(str "[Focus] No such goal: " ++ str (Names.Id.to_string id) ++ str ".")
   | FullyUnfocused ->
-    Pp.str "The proof is not focused"
-  | _ -> raise CErrors.Unhandled
+    Some (Pp.str "The proof is not focused")
+  | _ -> None
 end
 
 let check_cond_kind c k =
@@ -325,9 +325,9 @@ exception OpenProof of Names.Id.t option * open_error_reason
 let _ = CErrors.register_handler begin function
     | OpenProof (pid, reason) ->
       let open Pp in
-      Option.cata (fun pid ->
-          str " (in proof " ++ Names.Id.print pid ++ str "): ") (mt()) pid ++ print_open_error_reason reason
-    | _ -> raise CErrors.Unhandled
+      Some (Option.cata (fun pid ->
+          str " (in proof " ++ Names.Id.print pid ++ str "): ") (mt()) pid ++ print_open_error_reason reason)
+    | _ -> None
   end
 
 let warn_remaining_shelved_goals =
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
index 3ff0533b6b..d978885d62 100644
--- a/proofs/proof_bullet.ml
+++ b/proofs/proof_bullet.ml
@@ -79,8 +79,8 @@ module Strict = struct
       (function
       | FailedBullet (b,sugg) ->
         let prefix = Pp.(str"Wrong bullet " ++ pr_bullet b ++ str": ") in
-        Pp.(str "[Focus]" ++ spc () ++ prefix ++ suggest_on_error sugg)
-      | _ -> raise CErrors.Unhandled)
+        Some Pp.(str "[Focus]" ++ spc () ++ prefix ++ suggest_on_error sugg)
+      | _ -> None)
 
 
   (* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *)
@@ -203,7 +203,7 @@ exception SuggestNoSuchGoals of int * Proof.t
 let _ = CErrors.register_handler begin function
     | SuggestNoSuchGoals(n,proof) ->
       let suffix = suggest proof in
-      Pp.(str "No such " ++ str (CString.plural n "goal") ++ str "." ++
-          pr_non_empty_arg (fun x -> x) suffix)
-    | _ -> raise CErrors.Unhandled
+      Some (Pp.(str "No such " ++ str (CString.plural n "goal") ++ str "." ++
+                pr_non_empty_arg (fun x -> x) suffix))
+    | _ -> None
   end
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 ************************)
 (******************************************************************************)
diff --git a/tactics/declare.ml b/tactics/declare.ml
index ce2f3ec2c5..5655bdfd4d 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -24,10 +24,11 @@ exception AlreadyDeclared of (string option * Id.t)
 
 let _ = CErrors.register_handler (function
     | AlreadyDeclared (kind, id) ->
-      seq [ Pp.pr_opt_no_spc (fun s -> str s ++ spc ()) kind
-          ; Id.print id; str " already exists."]
+      Some
+        (seq [ Pp.pr_opt_no_spc (fun s -> str s ++ spc ()) kind
+             ; Id.print id; str " already exists."])
     | _ ->
-      raise CErrors.Unhandled)
+      None)
 
 module NamedDecl = Context.Named.Declaration
 
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml
index 72204e1d24..dbabc4e4e0 100644
--- a/tactics/pfedit.ml
+++ b/tactics/pfedit.ml
@@ -26,8 +26,8 @@ let use_unification_heuristics () = !use_unification_heuristics_ref
 
 exception NoSuchGoal
 let () = CErrors.register_handler begin function
-  | NoSuchGoal -> Pp.(str "No such goal.")
-  | _ -> raise CErrors.Unhandled
+  | NoSuchGoal -> Some Pp.(str "No such goal.")
+  | _ -> None
 end
 
 let get_nth_V82_goal p i =
diff --git a/topbin/coqtop_byte_bin.ml b/topbin/coqtop_byte_bin.ml
index 604c6e251a..7e977ca0f2 100644
--- a/topbin/coqtop_byte_bin.ml
+++ b/topbin/coqtop_byte_bin.ml
@@ -11,9 +11,9 @@
 (* We register this handler for lower-level toplevel loading code *)
 let _ = CErrors.register_handler (function
     | Symtable.Error e ->
-      Pp.str (Format.asprintf "%a" Symtable.report_error e)
+      Some (Pp.str (Format.asprintf "%a" Symtable.report_error e))
     | _ ->
-      raise CErrors.Unhandled
+      None
   )
 
 let drop_setup () =
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index d6db4a735c..a8bf4bc96f 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -848,8 +848,8 @@ let () = register_handler begin function
   let v = Tac2ffi.of_open (kn, args) in
   let t = GTypRef (Other t_exn, []) in
   let c = Tac2print.pr_valexpr (Global.env ()) Evd.empty v t in
-  hov 0 (str "Uncaught Ltac2 exception:" ++ spc () ++ hov 0 c)
-| _ -> raise Unhandled
+  Some (hov 0 (str "Uncaught Ltac2 exception:" ++ spc () ++ hov 0 c))
+| _ -> None
 end
 
 let () = CErrors.register_additional_error_info begin fun info ->
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index f6f6c4f1eb..07ec6ca1ba 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1356,6 +1356,12 @@ let explain_prim_token_notation_error kind env sigma = function
     Nota: explain_exn does NOT end with a newline anymore!
 *)
 
+exception Unhandled
+
+let wrap_unhandled f e =
+  try Some (f e)
+  with Unhandled -> None
+
 let explain_exn_default = function
   (* Basic interaction exceptions *)
   | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".")
@@ -1366,9 +1372,9 @@ let explain_exn_default = function
   | CErrors.Timeout -> hov 0 (str "Timeout!")
   | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.")
   (* Otherwise, not handled here *)
-  | _ -> raise CErrors.Unhandled
+  | _ -> raise Unhandled
 
-let _ = CErrors.register_handler explain_exn_default
+let _ = CErrors.register_handler (wrap_unhandled explain_exn_default)
 
 let rec vernac_interp_error_handler = function
   | Univ.UniverseInconsistency i ->
@@ -1409,6 +1415,6 @@ let rec vernac_interp_error_handler = function
   | Logic_monad.TacticFailure e ->
     vernac_interp_error_handler e
   | _ ->
-    raise CErrors.Unhandled
+    raise Unhandled
 
-let _ = CErrors.register_handler vernac_interp_error_handler
+let _ = CErrors.register_handler (wrap_unhandled vernac_interp_error_handler)
diff --git a/vernac/mltop.ml b/vernac/mltop.ml
index ab9d008659..5046248e11 100644
--- a/vernac/mltop.ml
+++ b/vernac/mltop.ml
@@ -99,9 +99,9 @@ let ocaml_toploop () =
 *)
 let _ = CErrors.register_handler (function
     | Dynlink.Error e ->
-      hov 0 (str "Dynlink error: " ++ str Dynlink.(error_message e))
+      Some (hov 0 (str "Dynlink error: " ++ str Dynlink.(error_message e)))
     | _ ->
-      raise CErrors.Unhandled
+      None
   )
 
 let ml_load s =
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 80b72225f0..3c70961e06 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -124,8 +124,8 @@ module Proof_global = struct
   let () =
     CErrors.register_handler begin function
       | NoCurrentProof ->
-        Pp.(str "No focused proof (No proof-editing in progress).")
-      | _ -> raise CErrors.Unhandled
+        Some (Pp.(str "No focused proof (No proof-editing in progress)."))
+      | _ -> None
     end
 
   open Lemmas