From 61edbfce11285443be098bbceddb7f8f04d2a5b0 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 30 Apr 2010 14:12:31 +0000
Subject: 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
---
 parsing/g_vernac.ml4 | 1 +
 parsing/ppvernac.ml  | 1 +
 2 files changed, 2 insertions(+)

(limited to 'parsing')

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)
-- 
cgit v1.2.3