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

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