diff options
| author | Enrico Tassi | 2014-01-06 17:59:06 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-01-06 17:59:06 +0100 |
| commit | 27d9da372a1c407221e687d9fb0d08fc6fca805f (patch) | |
| tree | 16c80c474d048217c25d5ea175728612ee2b9ee1 | |
| parent | 352ce04861c5dd849d20832a8fa0379ea8f43c8c (diff) | |
CoqIDE: do not unfocus if not needed on errors (closes: 3197)
| -rw-r--r-- | ide/coqOps.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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) |