aboutsummaryrefslogtreecommitdiff
path: root/generic/proof.el
diff options
context:
space:
mode:
authorThomas Kleymann1998-11-03 10:08:30 +0000
committerThomas Kleymann1998-11-03 10:08:30 +0000
commit6549a40f3ab0eefdcd827ed4449884239c0bf2b2 (patch)
treede6794cce42463104edca51b1cca1f2c8c2ab51e /generic/proof.el
parent19f16ac8eb742ff6337626b9d46c308ffa3e63a8 (diff)
A* Fix display handling problems (tms, all week)
Done. :-)
Diffstat (limited to 'generic/proof.el')
-rw-r--r--generic/proof.el35
1 files changed, 20 insertions, 15 deletions
diff --git a/generic/proof.el b/generic/proof.el
index 440c2ab8..ef3e68a6 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -151,21 +151,26 @@ The argument KBL is a list of tuples (k . f) where `k' is a keybinding
(defun proof-display-and-keep-buffer (buffer)
- "Display BUFFER and mark window according to `proof-window-dedicated-p'."
- (let ((window (get-buffer-window buffer 'visible)))
- (save-selected-window
- (save-excursion
- (display-buffer buffer)
- (set-window-dedicated-p (get-buffer-window buffer)
- proof-window-dedicated-p)
- (and window
- (progn (select-window window)
- ;; tms: I don't understand why the point in
- ;; proof-response-buffer is not at the end anyway.
- ;; Is there a superfluous save-excursion somewhere?
- (set-buffer buffer)
- (goto-char (point-max))
- (or (pos-visible-in-window-p) (recenter -1))))))))
+ "Display BUFFER and mark window according to `proof-window-dedicated-p'.
+
+Also ensures that point is visible."
+ (let (window)
+ (save-excursion
+ (set-buffer buffer)
+ (display-buffer buffer)
+ (setq window (get-buffer-window buffer 'visible))
+ (set-window-dedicated-p window proof-window-dedicated-p)
+ (and window
+ (save-selected-window
+ (select-window window)
+
+ ;; tms: I don't understand why the point in
+ ;; proof-response-buffer is not at the end anyway.
+ ;; Is there a superfluous save-excursion somewhere?
+ (goto-char (point-max))
+
+ (or (pos-visible-in-window-p (point) window)
+ (recenter -1)))))))
(defun proof-clean-buffer (buffer)
"Erase buffer and hide from display."