From 68553d59563cedbceed2986d01aa3d0f36733b89 Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Tue, 22 Oct 2013 14:31:42 +0000 Subject: 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 --- ide/coqOps.ml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) (limited to 'ide') 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; -- cgit v1.2.3