23 files changed, 336 insertions, 244 deletions
diff --git a/test-suite/ide/blocking-futures.fake b/test-suite/ide/blocking-futures.fake
new file mode 100644
index 00000000..b63f09bc
--- /dev/null
+++ b/test-suite/ide/blocking-futures.fake
@@ -0,0 +1,16 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Extraction will force the future computation, assert it is blocking
+# Example courtesy of Jonathan (jonikelee)
+#
+ADD { Require Import List. }
+ADD { Import ListNotations. }
+ADD { Definition myrev{A}(l : list A) : {rl : list A | rl = rev l}. }
+ADD { Proof. }
+ADD {   induction l. }
+ADD {    eexists; reflexivity. }
+ADD {    cbn; destruct IHl as [rl' H]; rewrite <-H; eexists; reflexivity. }
+ADD { Qed. }
+ADD { Extraction myrev. }
+GOALS
diff --git a/test-suite/ide/undo001.fake b/test-suite/ide/undo001.fake
index bbaea7e7..55263615 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 b855b6ea..5284c5d3 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 4c72e8dc..90757627 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 c2ddfb8c..9029b03e 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 525b9f2a..7e31c0b0 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 ed88bef5..cdfdee1b 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
deleted file mode 100644
index 87c06dbb..00000000
--- a/test-suite/ide/undo007.fake
+++ /dev/null
@@ -1,17 +0,0 @@
-# Script simulating a dialog between coqide and coqtop -ideslave
-# Run it via fake_ide
-#
-# 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.
diff --git a/test-suite/ide/undo008.fake b/test-suite/ide/undo008.fake
index 1c46c1e8..72cab7a3 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 47c77d23..76f400ef 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 4fe9df98..524416c3 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 cc85a764..0be439b2 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 f9b29ca1..b3d1c6d5 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 Fail Check bb.
-INTERPRAW Fail 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 3b1c61e6..f44156aa 100644
--- a/test-suite/ide/undo013.fake
+++ b/test-suite/ide/undo013.fake
@@ -2,30 +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 Lemma cc : False -> True.
-INTERP intro H.
-INTERP destruct H.
-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 5224b504..6d58b061 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 32e46ec9..ac17985a 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 2a6e512c..bdb81ecd 100644
--- a/test-suite/ide/undo016.fake
+++ b/test-suite/ide/undo016.fake
@@ -4,31 +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 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.
+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 232360e9..37423dc7 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 ef0945ab..11091bfa 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 70e70d7e..5df49ebb 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. }
diff --git a/test-suite/ide/undo020.fake b/test-suite/ide/undo020.fake
new file mode 100644
index 00000000..2adde908
--- /dev/null
+++ b/test-suite/ide/undo020.fake
@@ -0,0 +1,27 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# focusing a broken proof and fixing it
+ 
+# first proof
+ADD { Lemma a : True. }
+ADD { Proof using. }
+ADD here { idtac. }
+ADD { exact Ix. }
+ADD { Qed. }
+# second proof
+ADD { Lemma b : False. }
+ADD { Proof using. }
+ADD { admit. }
+ADD last { Qed. }
+# We join and expect some proof to fail
+WAIT
+# Going back to the error
+EDIT_AT here
+# Fixing the proof
+ADD { exact I. }
+ADD { Qed. }
+# we are back at the end
+ASSERT TIP last
+QUERY { Check a. }
+QUERY { Check b. }
diff --git a/test-suite/ide/undo021.fake b/test-suite/ide/undo021.fake
new file mode 100644
index 00000000..0d83ad25
--- /dev/null
+++ b/test-suite/ide/undo021.fake
@@ -0,0 +1,29 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# jumping between broken proofs
+ 
+# first proof
+ADD { Lemma a : True. }
+ADD { Proof using. }
+ADD here { idtac. }
+ADD { exact Ix. }
+ADD { Qed. }
+# second proof
+ADD { Lemma b : True. }
+ADD here2 { Proof using. }
+ADD { exact Ix. }
+ADD { Qed. }
+# We wait all slaves and expect both proofs to fail
+WAIT
+# Going back to the error
+EDIT_AT here2
+# this is not implemented yet, all after here is erased 
+EDIT_AT here
+# Fixing the proof
+ADD { exact I. }
+ADD last { Qed. }
+ASSERT TIP last
+# we are back at the end
+QUERY { Check a. }
+QUERY { Fail Check b. }
diff --git a/test-suite/ide/undo022.fake b/test-suite/ide/undo022.fake
new file mode 100644
index 00000000..51d8d106
--- /dev/null
+++ b/test-suite/ide/undo022.fake
@@ -0,0 +1,41 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# jumping between broken proofs + interp error while fixing.
+# the error should note make the GUI unfocus the currently focused proof.
+ 
+# first proof
+ADD { Lemma a : True /\ True. }
+ADD { Proof using. }
+ADD here { split. }
+ADD { exact Ix. } # first error
+ADD { exact Ix. } # second error
+ADD { Qed. }
+# second proof
+ADD { Lemma b : True. }
+ADD { Proof using. }
+ADD { exact I. }
+ADD last { Qed. }
+# We wait all slaves and expect both proofs to fail
+WAIT
+# Going back to the error
+EDIT_AT here
+# Fixing the proof
+ADD fix { exact I. }
+# showing the goals
+GOALS
+# re adding the wrong step
+ADD { exact Ix. }
+# showing the goals (failure) and retracting to the safe state suggested by Coq
+FAILGOALS
+# we assert we jumped back to the state immediately before the last (erroneous) 
+# one
+ASSERT TIP fix
+# finish off the proof
+ADD { exact I. }
+ADD { Qed. }
+# here we unfocus, hence we jump back to the end of the document
+ASSERT TIP last
+# we are back at the end
+QUERY { Check a. }
+QUERY { Check b. }