1 files changed, 24 insertions, 3 deletions
diff --git a/lib/errors.ml b/lib/errors.ml
index a4ec357e..c1d224df 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -69,12 +69,12 @@ let rec print_gen bottom stk e =
 let where = function
 | None -> mt ()
 | Some s ->
-  if !Flags.debug then str ("in "^s^":") ++ spc () else mt ()
+  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 ++ str "."
-  | Assert_failure _ | Match_failure _ -> str (Printexc.to_string e ^ ".")
-  | _ -> str ("Uncaught exception " ^ Printexc.to_string e ^ ".")
+  | 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 ()
@@ -99,6 +99,8 @@ let iprint (e, info) = print ~info e
 (** Same as [print], except that the "Please report" part of an anomaly
     isn't printed (used in Ltac debugging). *)
 let print_no_report e = print_gen (print_anomaly false) !handle_stack e
+let iprint_no_report (e, info) =
+  print_gen (print_anomaly false) !handle_stack e ++ print_backtrace info
 
 (** Predefined handlers **)
 
@@ -118,3 +120,22 @@ let noncritical = function
   | Timeout | Drop | Quit -> false
   | Invalid_argument "equal: functional value" -> false
   | _ -> true
+
+(** 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
+
+(** Prints info which is either an error or
+   an anomaly and then exits with the appropriate
+   error code *)
+
+let fatal_error info anomaly =
+  let msg = info ++ fnl () in
+  pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft msg;
+  flush_all ();
+  exit (if anomaly then 129 else 1)