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

19 files changed, 238 insertions, 233 deletions

diff --git a/test-suite/ide/undo001.fake b/test-suite/ide/undo001.fake
index bbaea7e7e..552636157 100644
--- a/test-suite/ide/undo001.fake
+++ b/test-suite/ide/undo001.fake
@@ -3,8 +3,8 @@
 #
 # Simple backtrack by 1 between two global definitions
 #
-INTERP Definition foo := 0.
-INTERP Definition bar := 1.
-REWIND 1
-INTERPRAW Check foo.
-INTERPRAW Fail Check bar.
+ADD here { Definition foo := 0. }
+ADD { Definition bar := 1. }
+EDIT_AT here
+QUERY { Check foo. }
+QUERY { Fail Check bar. }
diff --git a/test-suite/ide/undo002.fake b/test-suite/ide/undo002.fake
index b855b6ea7..5284c5d3a 100644
--- a/test-suite/ide/undo002.fake
+++ b/test-suite/ide/undo002.fake
@@ -3,8 +3,8 @@
 #
 # Simple backtrack by 2 before two global definitions
 #
-INTERP Definition foo := 0.
-INTERP Definition bar := 1.
-REWIND 2
-INTERPRAW Fail Check foo.
-INTERPRAW Fail Check bar.
+ADD { Definition foo := 0. }
+ADD { Definition bar := 1. }
+EDIT_AT initial
+QUERY { Fail Check foo. }
+QUERY { Fail Check bar. }
diff --git a/test-suite/ide/undo003.fake b/test-suite/ide/undo003.fake
index 4c72e8dc7..907576276 100644
--- a/test-suite/ide/undo003.fake
+++ b/test-suite/ide/undo003.fake
@@ -3,6 +3,6 @@
 #
 # Simple backtrack by 0 should be a no-op
 #
-INTERP Definition foo := 0.
-REWIND 0
-INTERPRAW Check foo.
+ADD here { Definition foo := 0. }
+EDIT_AT here
+QUERY { Check foo. }
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. }
diff --git a/test-suite/ide/undo005.fake b/test-suite/ide/undo005.fake
index 525b9f2a6..7e31c0b05 100644
--- a/test-suite/ide/undo005.fake
+++ b/test-suite/ide/undo005.fake
@@ -3,13 +3,13 @@
 #
 # Undoing arbitrary commands, as non-first step
 #
-INTERP Theorem b : O=O.
-INTERP assert True by trivial.
-INTERP Ltac g x := x.
+ADD { Theorem b : O=O. }
+ADD here { assert True by trivial. }
+ADD { Ltac g x := x. }
 # <replay>
-REWIND 1
+EDIT_AT here
 # <\replay>
-INTERP Ltac g x := x.
-INTERP assert True by trivial.
-INTERP trivial.
-INTERP Qed.
+ADD { Ltac g x := x. }
+ADD { assert True by trivial. }
+ADD { trivial. }
+ADD { Qed. }
diff --git a/test-suite/ide/undo006.fake b/test-suite/ide/undo006.fake
index ed88bef51..cdfdee1b7 100644
--- a/test-suite/ide/undo006.fake
+++ b/test-suite/ide/undo006.fake
@@ -4,11 +4,11 @@
 # Undoing declarations, as first step
 # Was bugged in 8.1
 #
-INTERP Theorem c : O=O.
-INTERP Inductive T : Type := I.
-REWIND 1
+ADD here { Theorem c : O=O. }
+ADD { Inductive T : Type := I. }
+EDIT_AT here
 # <replay>
-INTERP Inductive T : Type := I.
+ADD { Inductive T : Type := I. }
 # <\replay>
-INTERP trivial.
-INTERP Qed.
+ADD { trivial. }
+ADD { Qed. }
diff --git a/test-suite/ide/undo007.fake b/test-suite/ide/undo007.fake
index 87c06dbb3..770350fbd 100644
--- a/test-suite/ide/undo007.fake
+++ b/test-suite/ide/undo007.fake
@@ -4,14 +4,18 @@
 # Undoing declarations, as first step
 # new in 8.2
 #
-INTERP Theorem d : O=O.
-INTERP Definition e := O.
-INTERP Definition f := O.
-REWIND 1
-# <replay>
-INTERP Definition f := O.
-# <\replay>
-INTERP assert True by trivial.
-INTERP trivial.
-INTERP Qed.
-INTERPRAW Check e.
+ADD { Theorem d : O=O. }
+ADD here { Definition e := O. }
+ADD { Definition f := O. }
+
+# This is a bug in Stm undo, e is lost from master
+EDIT_AT here
+ADD { Definition f := O. }
+
+ADD { assert True by trivial. }
+ADD { exact (eq_refl e). }
+ADD { Qed. }
+ADD { Stm PrintDag. }
+ADD { Stm Finish. }
+QUERY { Print d. }
+QUERY { Check e. }
diff --git a/test-suite/ide/undo008.fake b/test-suite/ide/undo008.fake
index 1c46c1e87..72cab7a30 100644
--- a/test-suite/ide/undo008.fake
+++ b/test-suite/ide/undo008.fake
@@ -4,15 +4,15 @@
 # Undoing declarations, as non-first step
 # new in 8.2
 #
-INTERP Theorem h : O=O.
-INTERP assert True by trivial.
-INTERP Definition i := O.
-INTERP Definition j := O.
-REWIND 1
+ADD { Theorem h : O=O. }
+ADD { assert True by trivial. }
+ADD here { Definition i := O. }
+ADD { Definition j := O. }
+EDIT_AT here
 # <replay>
-INTERP Definition j := O.
+ADD { Definition j := O. }
 # <\replay>
-INTERP assert True by trivial.
-INTERP trivial.
-INTERP Qed.
-INTERPRAW Check i.
+ADD { assert True by trivial. }
+ADD { trivial. }
+ADD { Qed. }
+QUERY { Check i. }
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. }
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. }
diff --git a/test-suite/ide/undo011.fake b/test-suite/ide/undo011.fake
index cc85a764b..0be439b27 100644
--- a/test-suite/ide/undo011.fake
+++ b/test-suite/ide/undo011.fake
@@ -4,29 +4,31 @@
 # Bug 2082
 # Broken due to proof engine rewriting
 #
-INTERP Variable A : Prop.
-INTERP Variable B : Prop.
-INTERP Axiom OR : A \/ B.
-INTERP Lemma MyLemma2 : True.
-INTERP proof.
-INTERP per cases of (A \/ B) by OR.
-INTERP suppose A.
-INTERP     then (1 = 1).
-INTERP     then H1 : thesis.
-INTERP     thus thesis by H1.
-INTERP suppose B.
-REWIND 1
+ADD { Variable A : Prop. }
+ADD { Variable B : Prop. }
+ADD { Axiom OR : A \/ B. }
+ADD { Lemma MyLemma2 : True. }
+ADD { proof. }
+ADD { per cases of (A \/ B) by OR. }
+ADD { suppose A. }
+ADD {     then (1 = 1). }
+ADD there {     then H1 : thesis. }
+ADD here {     thus thesis by H1. }
+ADD { suppose B. }
+QUERY { Show. }
+EDIT_AT here
 # <replay>
-INTERP suppose B.
+ADD { suppose B. }
 # </replay>
-REWIND 2
+EDIT_AT there
 # <replay>
-INTERP     thus thesis by H1.
-INTERP suppose B.
+ADD {    thus thesis by H1. }
+ADD { suppose B. }
 # </replay>
-INTERP    then (1 = 1).
-INTERP    then H2 : thesis.
-INTERP    thus thesis by H2.
-INTERP end cases.
-INTERP end proof.
-INTERP Qed.
+QUERY { Show. }
+ADD {    then (1 = 1). }
+ADD {    then H2 : thesis. }
+ADD {    thus thesis by H2. }
+ADD { end cases. } 
+ADD { end proof. }
+ADD { Qed. }
diff --git a/test-suite/ide/undo012.fake b/test-suite/ide/undo012.fake
index 49169eba8..b3d1c6d53 100644
--- a/test-suite/ide/undo012.fake
+++ b/test-suite/ide/undo012.fake
@@ -2,25 +2,25 @@
 # Run it via fake_ide
 #
 # Test backtracking in presence of nested proofs
-# First, undoing the whole
 #
-INTERP Lemma aa : True -> True /\ True.
-INTERP intro H.
-INTERP split.
-INTERP Lemma bb : False -> False.
-INTERP intro H.
-INTERP apply H.
-INTERP Qed.
-INTERP apply H.
-INTERP Lemma cc : False -> True.
-INTERP intro H.
-INTERP destruct H.
-INTERP Qed.
-INTERP apply H.
-INTERP Qed.
-REWIND 1
-# We should now be just before aa, without opened proofs
-INTERPRAW Fail idtac.
-INTERPRAW Fail Check aa.
-INTERPRAW Check bb.
-INTERPRAW Check cc.
+ADD { Lemma aa : True -> True /\ True. }
+ADD { intro H. }
+ADD { split. }
+ADD { Lemma bb : False -> False. }
+ADD { intro H. }
+ADD { apply H. }
+ADD { Qed. }
+ADD { apply H. }
+ADD { Lemma cc : False -> True. }
+ADD { intro H. }
+ADD { destruct H. }
+ADD { Qed. }
+QUERY { Show. }
+ADD here { apply H. }
+ADD { Qed. }
+EDIT_AT here
+# We should now be just before the Qed.
+QUERY { Fail Check aa. }
+QUERY { Check bb. }
+QUERY { Check cc. }
+ADD { Qed. }
diff --git a/test-suite/ide/undo013.fake b/test-suite/ide/undo013.fake
index 389da2765..f44156aa3 100644
--- a/test-suite/ide/undo013.fake
+++ b/test-suite/ide/undo013.fake
@@ -2,27 +2,26 @@
 # Run it via fake_ide
 #
 # Test backtracking in presence of nested proofs
-# Second, trigger the full undo of an inner proof
+# Second, trigger the undo of an inner proof
 #
-INTERP Lemma aa : True -> True /\ True.
-INTERP intro H.
-INTERP split.
-INTERP Lemma bb : False -> False.
-INTERP intro H.
-INTERP apply H.
-INTERP Qed.
-INTERP apply H.
-INTERP Lemma cc : False -> True.
-INTERP intro H.
-INTERP destruct H.
-INTERP Qed.
-INTERP apply H.
-REWIND 2
-# We should now be just before "Lemma cc"
+ADD { Lemma aa : True -> True /\ True. }
+ADD { intro H. }
+ADD { split. }
+ADD { Lemma bb : False -> False. }
+ADD { intro H. }
+ADD { apply H. }
+ADD { Qed. }
+ADD { apply H. }
+ADD { Lemma cc : False -> True. }
+ADD { intro H. }
+ADD here { destruct H. }
+ADD { Qed. }
+ADD { apply H. }
+EDIT_AT here
 # <replay>
-INTERP Qed.
-INTERP apply H.
+ADD { Qed. }
+ADD { apply H. }
 # </replay>
-INTERP Qed.
-INTERPRAW Fail idtac.
-INTERPRAW Check (aa,bb,cc).
+ADD { Qed. }
+QUERY { Fail idtac. }
+QUERY { Check (aa,bb,cc). }
diff --git a/test-suite/ide/undo014.fake b/test-suite/ide/undo014.fake
index 5224b5045..6d58b061e 100644
--- a/test-suite/ide/undo014.fake
+++ b/test-suite/ide/undo014.fake
@@ -4,23 +4,23 @@
 # Test backtracking in presence of nested proofs
 # Third, undo inside an inner proof
 #
-INTERP Lemma aa : True -> True /\ True.
-INTERP intro H.
-INTERP split.
-INTERP Lemma bb : False -> False.
-INTERP intro H.
-INTERP apply H.
-INTERP Qed.
-INTERP apply H.
-INTERP Lemma cc : False -> True.
-INTERP intro H.
-INTERP destruct H.
-REWIND 1
+ADD { Lemma aa : True -> True /\ True. }
+ADD { intro H. }
+ADD { split. }
+ADD { Lemma bb : False -> False. }
+ADD { intro H. }
+ADD { apply H. }
+ADD { Qed. }
+ADD { apply H. }
+ADD { Lemma cc : False -> True. }
+ADD here { intro H. }
+ADD { destruct H. }
+EDIT_AT here
 # <replay>
-INTERP destruct H.
+ADD { destruct H. }
 # </replay>
-INTERP Qed.
-INTERP apply H.
-INTERP Qed.
-INTERPRAW Fail idtac.
-INTERPRAW Check (aa,bb,cc).
+ADD { Qed. }
+ADD { apply H. }
+ADD { Qed. }
+QUERY { Fail idtac. }
+QUERY { Check (aa,bb,cc). }
diff --git a/test-suite/ide/undo015.fake b/test-suite/ide/undo015.fake
index 32e46ec9a..ac17985aa 100644
--- a/test-suite/ide/undo015.fake
+++ b/test-suite/ide/undo015.fake
@@ -4,26 +4,26 @@
 # Test backtracking in presence of nested proofs
 # Fourth, undo from an inner proof to a above proof
 #
-INTERP Lemma aa : True -> True /\ True.
-INTERP intro H.
-INTERP split.
-INTERP Lemma bb : False -> False.
-INTERP intro H.
-INTERP apply H.
-INTERP Qed.
-INTERP apply H.
-INTERP Lemma cc : False -> True.
-INTERP intro H.
-INTERP destruct H.
-REWIND 4
+ADD { Lemma aa : True -> True /\ True. }
+ADD { intro H. }
+ADD { split. }
+ADD { Lemma bb : False -> False. }
+ADD { intro H. }
+ADD { apply H. }
+ADD here { Qed. }
+ADD { apply H. }
+ADD { Lemma cc : False -> True. }
+ADD { intro H. }
+ADD { destruct H. }
+EDIT_AT here
 # <replay>
-INTERP apply H.
-INTERP Lemma cc : False -> True.
-INTERP intro H.
-INTERP destruct H.
+ADD { apply H. }
+ADD { Lemma cc : False -> True. }
+ADD { intro H. }
+ADD { destruct H. }
 # </replay>
-INTERP Qed.
-INTERP apply H.
-INTERP Qed.
-INTERPRAW Fail idtac.
-INTERPRAW Check (aa,bb,cc).
+ADD { Qed. }
+ADD { apply H. }
+ADD { Qed. }
+QUERY { Fail idtac. }
+QUERY { Check (aa,bb,cc). }
diff --git a/test-suite/ide/undo016.fake b/test-suite/ide/undo016.fake
index a188e31b1..bdb81ecd9 100644
--- a/test-suite/ide/undo016.fake
+++ b/test-suite/ide/undo016.fake
@@ -4,29 +4,28 @@
 # Test backtracking in presence of nested proofs
 # Fifth, undo from an inner proof to a previous inner proof
 #
-INTERP Lemma aa : True -> True /\ True.
-INTERP intro H.
-INTERP split.
-INTERP Lemma bb : False -> False.
-INTERP intro H.
-INTERP apply H.
-INTERP Qed.
-INTERP apply H.
-INTERP Lemma cc : False -> True.
-INTERP intro H.
-INTERP destruct H.
-REWIND 6
-# We should be just before "Lemma bb"
+ADD { Lemma aa : True -> True /\ True. }
+ADD { intro H. }
+ADD { split. }
+ADD { Lemma bb : False -> False. }
+ADD here { intro H. }
+ADD { apply H. }
+ADD { Qed. }
+ADD { apply H. }
+ADD { Lemma cc : False -> True. }
+ADD { intro H. }
+ADD { destruct H. }
+EDIT_AT here
 # <replay>
-INTERP apply H.
-INTERP Qed.
-INTERP apply H.
-INTERP Lemma cc : False -> True.
-INTERP intro H.
-INTERP destruct H.
+ADD { apply H. }
+ADD { Qed. }
+ADD { apply H. }
+ADD { Lemma cc : False -> True. }
+ADD { intro H. }
+ADD { destruct H. }
 # </replay>
-INTERP Qed.
-INTERP apply H.
-INTERP Qed.
-INTERPRAW Fail idtac.
-INTERPRAW Check (aa,bb,cc).
+ADD { Qed. }
+ADD { apply H. }
+ADD { Qed. }
+QUERY { Fail idtac. }
+QUERY { Check (aa,bb,cc). }
diff --git a/test-suite/ide/undo017.fake b/test-suite/ide/undo017.fake
index 232360e9d..37423dc72 100644
--- a/test-suite/ide/undo017.fake
+++ b/test-suite/ide/undo017.fake
@@ -3,11 +3,11 @@
 #
 # bug #2569 : Undoing inside modules
 #
-INTERP Module M.
-INTERP Definition x := 0.
-INTERP End M.
-REWIND 1
+ADD { Module M. }
+ADD here { Definition x := 0. }
+ADD { End M. }
+EDIT_AT here
 # <replay>
-INTERP End M.
+ADD { End M. }
 # </replay>
-INTERPRAW Check M.x.
+QUERY { Check M.x. }
diff --git a/test-suite/ide/undo018.fake b/test-suite/ide/undo018.fake
index ef0945ab5..11091bfa6 100644
--- a/test-suite/ide/undo018.fake
+++ b/test-suite/ide/undo018.fake
@@ -3,11 +3,11 @@
 #
 # bug #2569 : Undoing inside section
 #
-INTERP Section M.
-INTERP Definition x := 0.
-INTERP End M.
-REWIND 1
+ADD { Section M. }
+ADD here { Definition x := 0. }
+ADD { End M. }
+EDIT_AT here
 # <replay>
-INTERP End M.
+ADD { End M. }
 # </replay>
-INTERPRAW Check x.
+QUERY { Check x. }
diff --git a/test-suite/ide/undo019.fake b/test-suite/ide/undo019.fake
index 70e70d7e4..5df49ebbb 100644
--- a/test-suite/ide/undo019.fake
+++ b/test-suite/ide/undo019.fake
@@ -3,12 +3,12 @@
 #
 # bug #2569 : Undoing a focused subproof
 #
-INTERP Goal True.
-INTERP {
-INTERP exact I.
-INTERP }
-REWIND 1
+ADD { Goal True. }
+ADD { \{ }
+ADD here { exact I. }
+ADD { \} }
+EDIT_AT here
 # <replay>
-INTERP }
+ADD { \} }
 # </replay>
-INTERP Qed.
+ADD { Qed. }