diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-05-26 22:33:23 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-05-26 22:33:23 +0000 |
| commit | 204256f7d5169f3b91329d4000fb794bec596b4c (patch) | |
| tree | 7dbf6bc19f9d3cec0e63801560873f8ff1def4fc /generic/proof-utils.el | |
| parent | faf0b7c14b57e399b1fe34e76eb8ddcd15e2bbad (diff) | |
Add proof state hover messages to proof script, along with useful customization.
Diffstat (limited to 'generic/proof-utils.el')
| -rw-r--r-- | generic/proof-utils.el | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/generic/proof-utils.el b/generic/proof-utils.el index 9e5ca52c..faf76474 100644 --- a/generic/proof-utils.el +++ b/generic/proof-utils.el @@ -408,12 +408,13 @@ NB: may change the selected window." ;; Return the window, hopefully the one we first thought of. (get-buffer-window buffer 0)) -(defun proof-display-and-keep-buffer (buffer &optional pos) +(defun proof-display-and-keep-buffer (buffer &optional pos force) "Display BUFFER and make window according to display mode. If optional POS is present, will set point to POS. Otherwise move point to the end of the buffer. Ensure that point is visible in window." - (save-excursion + (if (or force proof-auto-raise-buffers) + (save-excursion (save-selected-window (let ((window (proof-get-window-for-buffer buffer))) (if (window-live-p window) ;; [fails sometimes?] @@ -447,7 +448,7 @@ Ensure that point is visible in window." (unless mode-line-format ;; If the buffer gets displayed elsewhere, re-add ;; the modeline. - (kill-local-variable 'mode-line-format))))))))))) + (kill-local-variable 'mode-line-format)))))))))))) (defun proof-clean-buffer (buffer) "Erase buffer and hide from display if proof-delete-empty-windows set. |