diff options
author | 2011-04-15 18:57:21 +0000 | |
---|---|---|
committer | 2011-04-15 18:57:21 +0000 | |
commit | e760427024ac455a7fb10996fa6851c968bf6968 (patch) | |
tree | 524937fe81370d5ad8440500c3dd3cea65b329b4 /coq | |
parent | 3b5d51c37781b16e74fe7bab2e12c80dc86aa86a (diff) |
* fix coq-show-first-goal changing the current buffer
Diffstat (limited to 'coq')
-rw-r--r-- | coq/coq.el | 21 |
1 files changed, 10 insertions, 11 deletions
@@ -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 ")") |