diff options
author | 2013-03-12 23:59:02 +0000 | |
---|---|---|
committer | 2013-03-12 23:59:02 +0000 | |
commit | b66d099bdda2ce1cfaeeb7938346a348ef4d40cd (patch) | |
tree | 0a05f3bb096de81ac618bb93101c8d3a60969a86 | |
parent | 091824ae0f9bffcdee757bbd048e8a0f63cc5054 (diff) |
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
-rw-r--r-- | lib/errors.ml | 10 | ||||
-rw-r--r-- | lib/errors.mli | 7 |
2 files changed, 17 insertions, 0 deletions
diff --git a/lib/errors.ml b/lib/errors.ml index 92e5ac642..27baf4314 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 3e551e394..5f230d4c3 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 |