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

1 files changed, 20 insertions, 3 deletions

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]*")
     ]