diff options
| -rw-r--r-- | ide/coq.ml | 1 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 1 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 1 | ||||
| -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 |
8 files changed, 29 insertions, 1 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index 383a7a34c9..b1e8572bd3 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -109,6 +109,7 @@ let rec attribute_of_vernac_command = function (* Control *) | VernacTime com -> attribute_of_vernac_command com | VernacTimeout(_,com) -> attribute_of_vernac_command com + | VernacFail com -> attribute_of_vernac_command com | VernacList _ -> [] (* unsupported *) | VernacLoad _ -> [] diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 29b51322d2..a5b522feab 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -74,6 +74,7 @@ GEXTEND Gram vernac: FIRST [ [ IDENT "Time"; v = vernac -> VernacTime v | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v) + | IDENT "Fail"; v = vernac -> VernacFail v | locality; v = vernac_aux -> v ] ] ; vernac_aux: diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 99039e8672..a120253c18 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -531,6 +531,7 @@ let rec pr_vernac = function ++ spc()) else spc() ++ qs s | VernacTime v -> str"Time" ++ spc() ++ pr_vernac v | VernacTimeout(n,v) -> str"Timeout " ++ int n ++ spc() ++ pr_vernac v + | VernacFail v -> str"Fail" ++ spc() ++ pr_vernac v (* Syntax *) | VernacTacticNotation (n,r,e) -> pr_grammar_tactic_rule n ("",r,e) 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 |