From 27d9da372a1c407221e687d9fb0d08fc6fca805f Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 6 Jan 2014 17:59:06 +0100
Subject: CoqIDE: do not unfocus if not needed on errors (closes: 3197)

---
 ide/coqOps.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index ab70e35b98..be9075279b 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -625,7 +625,8 @@ object(self)
           if loc <> None then messages#push Error "Fixme LOC";
           messages#push Error msg;
           if Stateid.equal safe_id Stateid.dummy then self#show_goals
-          else undo safe_id (Doc.is_in_focus document safe_id))
+          else undo safe_id
+                 (Doc.focused document && Doc.is_in_focus document safe_id))
     in
       undo to_id unfocus_needed)
   
-- 
cgit v1.2.3