Document: undoing inside a focused zone does not require unfocusing

To test this fake_ide has also been improved with the GOALS command.
As for CoqIDE, ADDing a sentence does not force its evaluation.
The "advance 1 sentence" button is an ADD + GOALS.  If one of the
ADDed sentences is wrong, GOALS receives the error.  The GUI then
backtracks to a safe state id (sent by Coq).

fake_ide has GOALS (asserts that the goals call was OK) and FAILGOALS
to assert it fails and backtrack to a valid state. see unfdo022.fake.

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

3 files changed, 62 insertions, 4 deletions

diff --git a/ide/document.ml b/ide/document.ml
index 9b048320a..fab318f18 100644
--- a/ide/document.ml
+++ b/ide/document.ml
@@ -135,7 +135,7 @@ let find_id d f =
     | { state_id = Some id; data } when f id data -> Some id
     | _ -> None in
   try CList.find_map pred top, true with Not_found ->
-  try CList.find_map pred focus, focused d with Not_found ->
+  try CList.find_map pred focus, false with Not_found ->
       CList.find_map pred bot, true
 
 let before_tip d =
diff --git a/test-suite/ide/undo022.fake b/test-suite/ide/undo022.fake
new file mode 100644
index 000000000..51d8d106e
--- /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. }
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index c66db8bfe..5b6db94a4 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -212,9 +212,20 @@ module GUILogic = struct
         ignore(Document.cut_at doc id);
         print_document ()
   
-  let get_id id =
-    try Document.find_id doc (fun _ { name } -> name = id)
-    with Not_found -> error ("No state is named " ^ id)
+  let get_id_pred pred =
+    try Document.find_id doc pred
+    with Not_found -> error "No state found"
+
+  let get_id id = get_id_pred (fun _ { name } -> name = id)
+  
+  let after_fail coq = function
+    | Interface.Fail (safe_id,_,s) ->
+        prerr_endline "The command failed as expected";
+        let to_id, need_unfocus =
+          get_id_pred (fun id _ -> Stateid.equal id safe_id) in
+        after_edit_at (to_id, need_unfocus)
+          (base_eval_call (Serialize.edit_at to_id) coq)
+    | Interface.Good _ -> error "The command was expected to fail but did not"
 
 end
 
@@ -231,6 +242,10 @@ let eval_print l coq =
   | [ Tok(_,"ADD"); Top [Tok(_,name)]; Tok(_,phrase) ] ->
       let eid, tip = add_sentence ~name phrase in
       after_add (base_eval_call (add ((phrase,eid),(tip,true))) coq)
+  | [ Tok(_,"GOALS"); ] ->
+      eval_call (goals ()) coq
+  | [ Tok(_,"FAILGOALS"); ] ->
+      after_fail coq (base_eval_call ~fail:false (goals ()) coq)
   | [ Tok(_,"EDIT_AT"); Tok(_,id) ] ->
       let to_id, need_unfocus = get_id id in
       after_edit_at (to_id, need_unfocus) (base_eval_call (edit_at to_id) coq)
@@ -258,6 +273,8 @@ let grammar =
     ; Seq [Item (eat_rex "EDIT_AT"); Item eat_id]
     ; Seq [Item (eat_rex "QUERY"); Opt (Item eat_id); Item eat_phrase]
     ; Seq [Item (eat_rex "WAIT")]
+    ; Seq [Item (eat_rex "GOALS")]
+    ; Seq [Item (eat_rex "FAILGOALS")]
     ; Seq [Item (eat_rex "ASSERT"); Item (eat_rex "TIP"); Item eat_id ]
     ; Item (eat_rex "#[^\n]*")
     ]