CoqIDE: do not try to backtrack to a dummy id

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

1 files changed, 8 insertions, 5 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index af24d7f5f..6ea1678ac 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -603,7 +603,8 @@ object(self)
       | Fail (safe_id, loc, msg) ->
           if loc <> None then messages#push Error "Fixme LOC";
           messages#push Error msg;
-          undo safe_id (Doc.is_in_focus document safe_id))
+          if Stateid.equal safe_id Stateid.dummy then self#show_goals
+          else undo safe_id (Doc.is_in_focus document safe_id))
     in
       undo to_id unfocus_needed)
   
@@ -618,10 +619,12 @@ object(self)
     messages#clear;
     messages#push Error msg;
     ignore(self#process_feedback ());
-    Coq.seq
-      (self#backtrack_until ~move_insert:false
-        (fun id _ _ -> id = Some safe_id))
-      (Coq.lift (fun () -> script#recenter_insert))
+    if Stateid.equal safe_id Stateid.dummy then Coq.lift (fun () -> ())
+    else
+      Coq.seq
+        (self#backtrack_until ~move_insert:false
+          (fun id _ _ -> id = Some safe_id))
+        (Coq.lift (fun () -> script#recenter_insert))
 
   method backtrack_last_phrase =
     messages#clear;