fake_ide: speak the new protocol

A new syntax for .fake files, allowing multi line phrases and
labeled script points (to go back to them).

Test 7 fails because of a bug in STM (in a very spaghetti-like script).

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

1 files changed, 13 insertions, 12 deletions

diff --git a/test-suite/ide/undo009.fake b/test-suite/ide/undo009.fake
index 47c77d23d..76f400ef0 100644
--- a/test-suite/ide/undo009.fake
+++ b/test-suite/ide/undo009.fake
@@ -4,17 +4,18 @@
 # Undoing declarations, interleaved with proof steps
 # new in 8.2 *)
 #
-INTERP Theorem k : O=O.
-INTERP assert True by trivial.
-INTERP Definition l := O.
-INTERP assert True by trivial.
-INTERP Definition m := O.
-REWIND 3
+ADD { Theorem k : O=O. }
+ADD here { assert True by trivial. }
+ADD { Definition l := O. }
+ADD { assert True by trivial. }
+ADD { Definition m := O. }
+QUERY { Show. }
+EDIT_AT here
 # <replay>
-INTERP Definition l := O.
-INTERP assert True by trivial.
-INTERP Definition m := O.
+ADD { Definition l := O. }
+ADD { assert True by trivial. }
+ADD { Definition m := O. }
 # <\replay>
-INTERP assert True by trivial.
-INTERP trivial.
-INTERP Qed.
+ADD { assert True by trivial. }
+ADD { trivial. }
+ADD { Qed. }