The old code used switch-to-buffer, which is meant for changing the display, and had the side effect of putting the *goals* buffer first on the buffer-list. --- coq/coq.el | 28 ++++++++++++---------------- 1 files changed, 12 insertions(+), 16 deletions(-)
diff --git a/coq/coq.el b/coq/coq.el index fc22668..0a1e7f1 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -2075,22 +2075,18 @@ number of hypothesis displayed, without hiding the goal" (defun coq-update-minor-mode-alist () "Modify `minor-mode-alist' to display the number of subgoals in the modeline." - (save-window-excursion ; switch to buffer even if not visible - (switch-to-buffer proof-goals-buffer) - (let* ((nbgoals (string-to-number (first-word-of-buffer))) - (dummy (switch-to-buffer proof-script-buffer)) - (toclean (assq 'proof-active-buffer-fake-minor-mode minor-mode-alist))) - (while toclean ;; clean minor-mode-alist - (setq minor-mode-alist (remove toclean minor-mode-alist)) - (setq toclean (assq 'proof-active-buffer-fake-minor-mode minor-mode-alist))) - (setq minor-mode-alist - (append (list (list 'proof-active-buffer-fake-minor-mode - (coq-build-subgoals-string nbgoals))) - minor-mode-alist - ))))) - - - + (let ((nbgoals (with-current-buffer proof-goals-buffer + (string-to-number (first-word-of-buffer))))) + (with-current-buffer proof-script-buffer + (let ((toclean (assq 'proof-active-buffer-fake-minor-mode minor-mode-alist))) + (while toclean ;; clean minor-mode-alist + (setq minor-mode-alist (remove toclean minor-mode-alist)) + (setq toclean (assq 'proof-active-buffer-fake-minor-mode minor-mode-alist))) + (setq minor-mode-alist + (append (list (list 'proof-active-buffer-fake-minor-mode + (coq-build-subgoals-string nbgoals))) + minor-mode-alist + )))))) ;; This hook must be added before optim-resp-window, in order to be evaluated ;; *after* windows resizing. -- 1.7.6.1 _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
