Fail: a way to check that a command is refused without blocking a script

 "Fail cmd" is similar to "Time cmd", but instead of printing the execution time,
 it reverse the exit status of cmd. "Fail cmd" is successful iff cmd has ended with
 an error. This was, we can demonstrate erroneous commands in a script for
 pedagogical or testing purpose without having to comment it in order to play the rest
 of the script in coqide/PG.

  Coq < Fail Foo.
  The command has indeed failed with message:
  => Error: Unknown command of the non proof-editing mode.

  Coq < Fail Check Prop.
  Prop
     : Type
  Error: The command has not failed !

 Two more remarks:
 - Fail doesn't catch anomalies.
 - Yes it it possible to write things like Fail Fail ... :-)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12981 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 26 insertions, 1 deletions

diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 4fe2dffa8..0e2b3724c 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 4ef5401d8..e95c07c61 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 8386dd2b3..f88d7be79 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 1ec553a9a..b6cf215ec 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 cbd6fb8de..b8c8d261d 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