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

diff --git a/test-suite/ide/undo010.fake b/test-suite/ide/undo010.fake
index 4fe9df986..524416c32 100644
--- a/test-suite/ide/undo010.fake
+++ b/test-suite/ide/undo010.fake
@@ -4,25 +4,25 @@
 # Undoing declarations, interleaved with proof steps and commands *)
 # new in 8.2 *)
 #
-INTERP Theorem n : O=O.
-INTERP assert True by trivial.
-INTERP Definition o := O.
-INTERP Ltac h x := x.
-INTERP assert True by trivial.
-INTERP Focus.
-INTERP Definition p := O.
-REWIND 1
-REWIND 1
-REWIND 1
-REWIND 1
-REWIND 1
+ADD { Theorem n : O=O. }
+ADD s2 { assert True by trivial. }
+ADD s3 { Definition o := O. }
+ADD s4 { Ltac h x := x. }
+ADD s5 { assert True by trivial. }
+ADD s6 { Focus. }
+ADD { Definition p := O. }
+EDIT_AT s6
+EDIT_AT s5
+EDIT_AT s4
+EDIT_AT s3
+EDIT_AT s2
 # <replay>
-INTERP Definition o := O.
-INTERP Ltac h x := x.
-INTERP assert True by trivial.
-INTERP Focus.
-INTERP Definition p := O.
+ADD { Definition o := O. }
+ADD { Ltac h x := x. }
+ADD { assert True by trivial. } 
+ADD { Focus. }
+ADD { Definition p := O. }
 # </replay>
-INTERP assert True by trivial.
-INTERP trivial.
-INTERP Qed.
+ADD { assert True by trivial. }
+ADD { trivial. }
+ADD { Qed. }