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, 7 insertions, 7 deletions

diff --git a/test-suite/ide/undo004.fake b/test-suite/ide/undo004.fake
index c2ddfb8cb..9029b03e2 100644
--- a/test-suite/ide/undo004.fake
+++ b/test-suite/ide/undo004.fake
@@ -3,12 +3,12 @@
 #
 # Undoing arbitrary commands, as first step
 #
-INTERP Theorem a : O=O.
-INTERP Ltac f x := x.
-REWIND 1
+ADD here { Theorem a : O=O. }
+ADD { Ltac f x := x. }
+EDIT_AT here
 # <replay>
-INTERP Ltac f x := x.
+ADD { Ltac f x := x. }
 # <\replay>
-INTERP assert True by trivial.
-INTERP trivial.
-INTERP Qed.
+ADD { assert True by trivial. }
+ADD { trivial. }
+ADD { Qed. }