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
---
 ide/coq.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'ide')

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 _ -> []
 
-- 
cgit v1.2.3