From b66d099bdda2ce1cfaeeb7938346a348ef4d40cd Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 12 Mar 2013 23:59:02 +0000
Subject: New function Errors.noncritical for restricting try ... with ...

 For the moment, are considered critical :

  Sys.Break, Stack_overflow, Out_of_memory
  Assert_failure, Match_failure, Anomaly, Timeout, Drop, Exit

 These exceptions should normally *not* be catched by a "try",
 hence the suggested code for generic "try":

  try ... with e when Errors.noncritical e -> ...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16269 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/errors.ml  | 10 ++++++++++
 lib/errors.mli |  7 +++++++
 2 files changed, 17 insertions(+)

diff --git a/lib/errors.ml b/lib/errors.ml
index 92e5ac6423..27baf4314f 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -124,3 +124,13 @@ let _ = register_handler begin function
   | UserError(s,pps) -> hov 0 (str "Error: " ++ where (Some s) ++ pps)
   | _ -> raise Unhandled
 end
+
+(** Critical exceptions shouldn't be catched and ignored by mistake
+    by inner functions during a [vernacinterp]. They should be handled
+    only at the very end of interp, to be displayed to the user. *)
+
+let noncritical = function
+  | Sys.Break | Out_of_memory | Stack_overflow
+  | Assert_failure _ | Match_failure _ | Anomaly _
+  | Timeout | Drop | Quit -> false
+  | _ -> true
diff --git a/lib/errors.mli b/lib/errors.mli
index 3e551e394c..5f230d4c3b 100644
--- a/lib/errors.mli
+++ b/lib/errors.mli
@@ -90,3 +90,10 @@ val print_no_report : exn -> Pp.std_ppcmds
 (** Same as [print], except that anomalies are not printed but re-raised
     (used for the Fail command) *)
 val print_no_anomaly : exn -> Pp.std_ppcmds
+
+(** Critical exceptions shouldn't be catched and ignored by mistake
+    by inner functions during a [vernacinterp]. They should be handled
+    only at the very end of interp, to be displayed to the user.
+    Typical example: [Sys.Break], [Assert_failure], [Anomaly] ...
+*)
+val noncritical : exn -> bool
-- 
cgit v1.2.3