diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/cerrors.ml | 3 | ||||
| -rw-r--r-- | toplevel/cerrors.mli | 6 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 15 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 1 |
5 files changed, 26 insertions, 1 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 4fe2dffa8c..0e2b3724ce 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -162,3 +162,6 @@ let _ = Tactic_debug.explain_logic_error_no_anomaly := let explain_exn_function = ref explain_exn_default let explain_exn e = !explain_exn_function e + +let explain_exn_no_anomaly e = + explain_exn_default_aux (fun () -> raise e) mt e diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli index 4ef5401d8a..e95c07c61a 100644 --- a/toplevel/cerrors.mli +++ b/toplevel/cerrors.mli @@ -15,6 +15,12 @@ val print_loc : loc -> std_ppcmds val explain_exn : exn -> std_ppcmds +(** Same, but will re-raise all anomalies instead of explaining them *) + +val explain_exn_no_anomaly : exn -> std_ppcmds + +(** For debugging purpose (?), the explain function can be twicked *) + val explain_exn_function : (exn -> std_ppcmds) ref val explain_exn_default : exn -> std_ppcmds diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 8386dd2b32..f88d7be795 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -23,6 +23,8 @@ open Ppvernac exception DuringCommandInterp of Util.loc * exn +exception HasNotFailed + (* Specifies which file is read. The intermediate file names are discarded here. The Drop exception becomes an error. We forget if the error ocurred during interpretation or not *) @@ -158,6 +160,19 @@ let rec vernac_com interpfun (loc,com) = | VernacList l -> List.iter (fun (_,v) -> interp v) l + | VernacFail v -> + if not !just_parsing then begin try + interp v; raise HasNotFailed + with e -> match real_error e with + | HasNotFailed -> + errorlabstrm "Fail" (str "The command has not failed !") + | e -> + (* if [e] is an anomaly, the next function will re-raise it *) + let msg = Cerrors.explain_exn_no_anomaly e in + msgnl (str "The command has indeed failed with message:" ++ + fnl () ++ str "=> " ++ hov 0 msg) + end + | VernacTime v -> if not !just_parsing then begin let tstart = System.get_time() in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 1ec553a9a0..b6cf215ec2 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1292,7 +1292,7 @@ let vernac_check_guard () = let interp c = match c with (* Control (done in vernac) *) - | (VernacTime _ | VernacList _ | VernacLoad _| VernacTimeout _) -> + | (VernacTime _|VernacList _|VernacLoad _|VernacTimeout _|VernacFail _) -> assert false (* Syntax *) diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index cbd6fb8dec..b8c8d261d6 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -208,6 +208,7 @@ type vernac_expr = | VernacLoad of verbose_flag * string | VernacTime of vernac_expr | VernacTimeout of int * vernac_expr + | VernacFail of vernac_expr (* Syntax *) | VernacTacticNotation of int * grammar_tactic_prod_item_expr list * raw_tactic_expr |