Merge PR #10380: [errors] remove "is_handled" logic, turn unhandled into anomalies

Reviewed-by: SkySkimmer
Reviewed-by: gares

10 files changed, 57 insertions, 69 deletions

diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index e6219e4eeb..a42504701f 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -31,10 +31,6 @@ let make_anomaly ?label pp =
 let anomaly ?loc ?label pp =
   Loc.raise ?loc (Anomaly (label, pp))
 
-let is_anomaly = function
-| Anomaly _ -> true
-| _ -> false
-
 exception UserError of string option * Pp.t (* User errors *)
 
 let todo s = prerr_string ("TODO: "^s^"\n")
@@ -54,6 +50,14 @@ 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
+  List.exists is_handled_by !handle_stack
+
+let is_anomaly = function
+| Anomaly _ -> true
+| exn -> not (is_handled exn)
+
 (** [print_gen] is a general exception printer which tries successively
     all the handlers of a list, and finally a [bottom] handler if all
     others have failed *)
@@ -77,9 +81,12 @@ let where = function
   if !Flags.debug then str "in " ++ str s ++ str ":" ++ spc () else mt ()
 
 let raw_anomaly e = match e with
-  | Anomaly (s, pps) -> where s ++ pps
-  | Assert_failure _ | Match_failure _ -> str (Printexc.to_string e) ++ str "."
-  | _ -> str "Uncaught exception " ++ str (Printexc.to_string e) ++ str "."
+  | Anomaly (s, pps) ->
+    where s ++ pps
+  | Assert_failure _ | Match_failure _ ->
+    str (Printexc.to_string e) ++ str "."
+  | _ ->
+    str "Uncaught exception " ++ str (Printexc.to_string e) ++ str "."
 
 let print_backtrace e = match Backtrace.get_backtrace e with
 | None -> mt ()
@@ -128,12 +135,3 @@ let noncritical = function
   | Invalid_argument "equal: functional value" -> false
   | _ -> true
 [@@@ocaml.warning "+52"]
-
-(** Check whether an exception is handled *)
-
-exception Bottom
-
-let handled e =
-  let bottom _ = raise Bottom in
-  try let _ = print_gen bottom !handle_stack e in true
-  with Bottom -> false
diff --git a/lib/cErrors.mli b/lib/cErrors.mli
index 8bb161d745..51ec5c907a 100644
--- a/lib/cErrors.mli
+++ b/lib/cErrors.mli
@@ -89,7 +89,3 @@ val iprint_no_report : Exninfo.iexn -> Pp.t
     Typical example: [Sys.Break], [Assert_failure], [Anomaly] ...
 *)
 val noncritical : exn -> bool
-
-(** Check whether an exception is handled by some toplevel printer. The
-    [Anomaly] exception is never handled. *)
-val handled : exn -> bool
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 778aaf8886..7e3759f177 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -10,7 +10,7 @@
 
 let fatal_error exn =
   Topfmt.(in_phase ~phase:ParsingCommandLine print_err_exn exn);
-  let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in
+  let exit_code = if (CErrors.is_anomaly exn) then 129 else 1 in
   exit exit_code
 
 let error_wrong_arg msg =
diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml
index 64d8e69121..a04552e8db 100644
--- a/toplevel/coqc.ml
+++ b/toplevel/coqc.ml
@@ -62,7 +62,5 @@ let main () =
     flush_all();
     Topfmt.print_err_exn exn;
     flush_all();
-    let exit_code =
-      if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1
-    in
+    let exit_code = if (CErrors.is_anomaly exn) then 129 else 1 in
     exit exit_code
diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml
index d3cdeb3e7b..5cced2baac 100644
--- a/toplevel/coqcargs.ml
+++ b/toplevel/coqcargs.ml
@@ -48,7 +48,7 @@ let depr opt =
 (* XXX Remove this duplication with Coqargs *)
 let fatal_error exn =
   Topfmt.(in_phase ~phase:ParsingCommandLine print_err_exn exn);
-  let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in
+  let exit_code = if (CErrors.is_anomaly exn) then 129 else 1 in
   exit exit_code
 
 let error_missing_arg s =
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 5283130bc9..e43e6a8da4 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -103,7 +103,7 @@ let fatal_error_exn exn =
   Topfmt.(in_phase ~phase:Initialization print_err_exn exn);
   flush_all ();
   let exit_code =
-    if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1
+    if (CErrors.is_anomaly exn) then 129 else 1
   in
   exit exit_code
 
diff --git a/user-contrib/Ltac2/tac2print.ml b/user-contrib/Ltac2/tac2print.ml
index 68c39da9aa..b89067086f 100644
--- a/user-contrib/Ltac2/tac2print.ml
+++ b/user-contrib/Ltac2/tac2print.ml
@@ -473,7 +473,7 @@ end
 
 let () = register_init "err" begin fun _ _ e ->
   let e = to_ext val_exn e in
-  let (e, _) = ExplainErr.process_vernac_interp_error ~allow_uncaught:true e in
+  let (e, _) = ExplainErr.process_vernac_interp_error e in
   str "err:(" ++ CErrors.print_no_report e ++ str ")"
 end
 
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index ec7333aa43..5c5a4ffbcb 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -44,57 +44,61 @@ let explain_exn_default = function
 let _ = CErrors.register_handler explain_exn_default
 
 
-(** Pre-explain a vernac interpretation error *)
-
-let wrap_vernac_error (exn, info) strm = (EvaluatedError (strm, None), info)
-
-let process_vernac_interp_error exn = match fst exn with
+let vernac_interp_error_handler = function
   | Univ.UniverseInconsistency i ->
     let msg =
       if !Constrextern.print_universes then
-	str "." ++ spc() ++ 
-          Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i
+        str "." ++ spc() ++
+        Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i
       else
 	mt() in
-    wrap_vernac_error exn (str "Universe inconsistency" ++ msg ++ str ".")
+    str "Universe inconsistency" ++ msg ++ str "."
   | TypeError(ctx,te) ->
-      let te = map_ptype_error EConstr.of_constr te in
-      wrap_vernac_error exn (Himsg.explain_type_error ctx Evd.empty te)
+    let te = map_ptype_error EConstr.of_constr te in
+    Himsg.explain_type_error ctx Evd.empty te
   | PretypeError(ctx,sigma,te) ->
-      wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te)
+    Himsg.explain_pretype_error ctx sigma te
   | Notation.PrimTokenNotationError(kind,ctx,sigma,te) ->
-      wrap_vernac_error exn (Himsg.explain_prim_token_notation_error kind ctx sigma te)
+    Himsg.explain_prim_token_notation_error kind ctx sigma te
   | Typeclasses_errors.TypeClassError(env, sigma, te) ->
-      wrap_vernac_error exn (Himsg.explain_typeclass_error env sigma te)
+    Himsg.explain_typeclass_error env sigma te
   | InductiveError e ->
-      wrap_vernac_error exn (Himsg.explain_inductive_error e)
+    Himsg.explain_inductive_error e
   | Modops.ModuleTypingError e ->
-      wrap_vernac_error exn (Himsg.explain_module_error e)
+    Himsg.explain_module_error e
   | Modintern.ModuleInternalizationError e ->
-      wrap_vernac_error exn (Himsg.explain_module_internalization_error e)
+    Himsg.explain_module_internalization_error e
   | RecursionSchemeError (env,e) ->
-      wrap_vernac_error exn (Himsg.explain_recursion_scheme_error env e)
+    Himsg.explain_recursion_scheme_error env e
   | Cases.PatternMatchingError (env,sigma,e) ->
-      wrap_vernac_error exn (Himsg.explain_pattern_matching_error env sigma e)
+    Himsg.explain_pattern_matching_error env sigma e
   | Tacred.ReductionTacticError e ->
-      wrap_vernac_error exn (Himsg.explain_reduction_tactic_error e)
+    Himsg.explain_reduction_tactic_error e
   | Logic.RefinerError (env, sigma, e) ->
-    wrap_vernac_error exn (Himsg.explain_refiner_error env sigma e)
+    Himsg.explain_refiner_error env sigma e
   | Nametab.GlobalizationError q ->
-      wrap_vernac_error exn
-        (str "The reference" ++ spc () ++ Libnames.pr_qualid q ++
-	 spc () ++ str "was not found" ++
-	 spc () ++ str "in the current" ++ spc () ++ str "environment.")
+    str "The reference" ++ spc () ++ Libnames.pr_qualid q ++
+    spc () ++ str "was not found" ++
+    spc () ++ str "in the current" ++ spc () ++ str "environment."
   | Refiner.FailError (i,s) ->
-      let s = Lazy.force s in
-      wrap_vernac_error exn
-	(str "Tactic failure" ++
-         (if Pp.ismt s then s else str ": " ++ s) ++
-         if Int.equal i 0 then str "." else str " (level " ++ int i ++ str").")
+    let s = Lazy.force s in
+    str "Tactic failure" ++
+    (if Pp.ismt s then s else str ": " ++ s) ++
+    if Int.equal i 0 then str "." else str " (level " ++ int i ++ str")."
   | AlreadyDeclared msg ->
-      wrap_vernac_error exn (msg ++ str ".")
+    msg ++ str "."
   | _ ->
-      exn
+    raise CErrors.Unhandled
+
+let _ = CErrors.register_handler vernac_interp_error_handler
+
+(** Pre-explain a vernac interpretation error *)
+
+let wrap_vernac_error (exn, info) strm = (EvaluatedError (strm, None), info)
+
+let process_vernac_interp_error exn =
+  try vernac_interp_error_handler (fst exn) |> wrap_vernac_error exn
+  with CErrors.Unhandled -> exn
 
 let rec strip_wrapping_exceptions = function
   | Logic_monad.TacticFailure e ->
@@ -106,16 +110,9 @@ let additional_error_info = ref []
 let register_additional_error_info f =
   additional_error_info := f :: !additional_error_info
 
-let process_vernac_interp_error ?(allow_uncaught=true) (exc, info) =
+let process_vernac_interp_error (exc, info) =
   let exc = strip_wrapping_exceptions exc in
   let e = process_vernac_interp_error (exc, info) in
-  let () =
-    if not allow_uncaught && not (CErrors.handled (fst e)) then
-      let (e, info) = e in
-      let msg = str "Uncaught exception " ++ str (Printexc.to_string e) ++ str "." in
-      let err = CErrors.make_anomaly msg in
-      Util.iraise (err, info)
-  in
   let e' =
     try Some (CList.find_map (fun f -> f e) !additional_error_info)
     with _ -> None
diff --git a/vernac/explainErr.mli b/vernac/explainErr.mli
index eb956f2e60..cc2a130925 100644
--- a/vernac/explainErr.mli
+++ b/vernac/explainErr.mli
@@ -13,7 +13,7 @@ exception EvaluatedError of Pp.t * exn option
 
 (** Pre-explain a vernac interpretation error *)
 
-val process_vernac_interp_error : ?allow_uncaught:bool -> Util.iexn -> Util.iexn
+val process_vernac_interp_error : Util.iexn -> Util.iexn
 
 (** General explain function. Should not be used directly now,
     see instead function [Errors.print] and variants *)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ca7f7ffa0b..ac47a6a8f3 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2308,8 +2308,7 @@ let with_fail ~st f =
     | HasNotFailed as e -> raise e
     | e when CErrors.noncritical e || e = Timeout ->
       let e = CErrors.push e in
-      raise (HasFailed (CErrors.iprint
-                          (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e)))
+      raise (HasFailed (CErrors.iprint (ExplainErr.process_vernac_interp_error e)))
   with e when CErrors.noncritical e ->
     (* Restore the previous state XXX Careful here with the cache! *)
     Vernacstate.invalidate_cache ();