Merge PR #11498: [exn] Forbid raising in exn printers, make them return Pp.t option

Reviewed-by: ppedrot

16 files changed, 82 insertions, 74 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 6df3378524..1caf2c2722 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 690b1620b9..a26ce71141 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..323dc8c1a4 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
@@ -88,30 +86,31 @@ let register_additional_error_info (f : Exninfo.info -> (Pp.t option Loc.located
     all the handlers of a list, and finally a [bottom] handler if all
     others have failed *)
 
-let rec print_gen ~anomaly ~extra_msg stk (e, info) =
+let rec print_gen ~anomaly ~extra_msg stk e =
   match stk with
   | [] ->
     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
 
 let print_gen ~anomaly (e, info) =
   let extra_info =
     try CList.find_map (fun f -> Some (f info)) !additional_error_info_handler
     with Not_found -> None
   in
-  let extra_msg, info = match extra_info with
-    | None -> None, info
-    | Some (loc, msg) ->
-      let info = Option.cata (fun l -> Loc.add_loc info l) info loc in
-      msg, info
+  let extra_msg = match extra_info with
+    | None -> None
+    | Some (loc, msg) -> msg
   in
-  print_gen ~anomaly ~extra_msg !handle_stack (e,info)
+  try
+    print_gen ~anomaly ~extra_msg !handle_stack e
+  with exn ->
+    (* exception in error printer *)
+    str "<in exception printer>" ++ fnl () ++ print_anomaly anomaly exn
 
 (** The standard exception printer *)
 let iprint (e, info) =
@@ -130,8 +129,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 70cba858c9..2a0c109a42 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