diff options
| author | Pierre-Marie Pédrot | 2015-05-18 17:47:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-05-18 19:04:32 +0200 |
| commit | ea3909466eaaf86ff212c0a002e5df11e4a979f5 (patch) | |
| tree | 2fd23c2ffa95c3bcfcd5c3e15404716dbc4df283 /toplevel | |
| parent | b994685d85d30f0db8ee0ec10f802f6bf3797e4b (diff) | |
The Fail command does not catch uncaught exception anomalies anymore.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/cerrors.ml | 9 | ||||
| -rw-r--r-- | toplevel/cerrors.mli | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
3 files changed, 10 insertions, 3 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index a0892bed9a..accba3121b 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -110,9 +110,16 @@ let rec strip_wrapping_exceptions = function strip_wrapping_exceptions e | exc -> exc -let process_vernac_interp_error ?(with_header=true) (exc, info) = +let process_vernac_interp_error ?(allow_uncaught=true) ?(with_header=true) (exc, info) = let exc = strip_wrapping_exceptions exc in let e = process_vernac_interp_error with_header (exc, info) in + let () = + if not allow_uncaught && not (Errors.handled (fst e)) then + let (e, info) = e in + let msg = str "Uncaught exception " ++ str (Printexc.to_string e) in + let err = Errors.make_anomaly msg in + Util.iraise (err, info) + in let ltac_trace = Exninfo.get info Proof_type.ltac_trace_info in let loc = Option.default Loc.ghost (Loc.get_loc info) in match ltac_trace with diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli index 100b3772cc..729686f32d 100644 --- a/toplevel/cerrors.mli +++ b/toplevel/cerrors.mli @@ -12,7 +12,7 @@ val print_loc : Loc.t -> Pp.std_ppcmds (** Pre-explain a vernac interpretation error *) -val process_vernac_interp_error : ?with_header:bool -> Util.iexn -> Util.iexn +val process_vernac_interp_error : ?allow_uncaught:bool -> ?with_header:bool -> Util.iexn -> Util.iexn (** General explain function. Should not be used directly now, see instead function [Errors.print] and variants *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 9d5edc80a0..849b1d47d6 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -2106,7 +2106,7 @@ let with_fail b f = | e -> let e = Errors.push e in raise (HasFailed (Errors.iprint - (Cerrors.process_vernac_interp_error ~with_header:false e)))) + (Cerrors.process_vernac_interp_error ~allow_uncaught:false ~with_header:false e)))) () with e when Errors.noncritical e -> let (e, _) = Errors.push e in |