From e760427024ac455a7fb10996fa6851c968bf6968 Mon Sep 17 00:00:00 2001
From: Hendrik Tews
Date: Fri, 15 Apr 2011 18:57:21 +0000
Subject: * fix coq-show-first-goal changing the current buffer

---
 coq/coq.el | 21 ++++++++++-----------
 1 file changed, 10 insertions(+), 11 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index c2709f6f..12dad414 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -2054,17 +2054,16 @@ buffer."
 First goal is displayed on the bottom of its window, maximizing the
 number of hypothesis displayed, without hiding the goal"
   (interactive)
-  (let* ((curwin (selected-window))
-         (goalbuf (get-buffer-window proof-goals-buffer)))
-    (if (eq goalbuf nil) ()
-      (select-window goalbuf)
-      (search-forward-regexp "subgoal 2\\|\\'"); find snd goal or buffer end
-      (beginning-of-line)
-      (ignore-errors (search-backward-regexp "\\S-")) ; find something else than a space
-      (recenter (- 1)) ; put it at bottom og window
-      (beginning-of-line)
-      (select-window curwin)
-      )))
+  (let ((goal-win (get-buffer-window proof-goals-buffer)))
+    (if goal-win
+        (with-selected-window goal-win
+          ;; find snd goal or buffer end
+          (search-forward-regexp "subgoal 2\\|\\'")
+          (beginning-of-line)
+          ;; find something else than a space
+          (ignore-errors (search-backward-regexp "\\S-"))
+          (recenter (- 1)) ; put it at bottom og window
+          (beginning-of-line)))))
 
 (defvar coq-modeline-string2 ")")
 (defvar coq-modeline-string1 ")")
-- 
cgit v1.2.3