Attempt to prevent recording of buffer switching history (display-buffer cannot be stopped, sadly)

2 files changed, 63 insertions, 3 deletions

diff --git a/generic/proof-compat.el b/generic/proof-compat.el
index 5a41b04c..dd5d541c 100644
--- a/generic/proof-compat.el
+++ b/generic/proof-compat.el
@@ -389,6 +389,61 @@ The modified ALIST is returned."
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;
+;;; Attempt to harmonise pop-to-buffer behaviour 
+;;;
+
+(if proof-running-on-Emacs21
+    ;; NB: GNU Emacs version has fewer args
+    (defalias 'pg-pop-to-buffer 'pop-to-buffer))
+
+(if proof-running-on-XEmacs
+;; Version from XEmacs 21.4.12, with args to match GNU Emacs
+;; NB: GNU Emacs version has fewer args, we don't use ON-FRAME
+(defun pg-pop-to-buffer (bufname &optional not-this-window-p no-record on-frame)
+  "Select buffer BUFNAME in some window, preferably a different one.
+If BUFNAME is nil, then some other buffer is chosen.
+If `pop-up-windows' is non-nil, windows can be split to do this.
+If optional second arg NOT-THIS-WINDOW-P is non-nil, insist on finding
+another window even if BUFNAME is already visible in the selected window.
+If optional fourth arg is non-nil, it is the frame to pop to this
+buffer on.
+If optional third arg is non-nil, do not record this in switching history.
+(addition for PG).
+
+If `focus-follows-mouse' is non-nil, keyboard focus is left unchanged."
+  (let ((oldbuf (current-buffer))
+	buf window frame)
+    (if (null bufname)
+	(setq buf (other-buffer (current-buffer)))
+      (setq buf (get-buffer bufname))
+      (if (null buf)
+	  (progn
+	    (setq buf (get-buffer-create bufname))
+	    (set-buffer-major-mode buf))))
+    (push-window-configuration)
+    (set-buffer buf)
+    (setq window (display-buffer buf not-this-window-p on-frame))
+    (setq frame (window-frame window))
+    ;; if the display-buffer hook decided to show this buffer in another
+    ;; frame, then select that frame, (unless obeying focus-follows-mouse -sb).
+    (if (and (not focus-follows-mouse)
+	     (not (eq frame (selected-frame))))
+	(select-frame frame))
+    (unless no-record (record-buffer buf))
+    (if (and focus-follows-mouse
+	     on-frame
+	     (not (eq on-frame (selected-frame))))
+	(set-buffer oldbuf)
+      ;; select-window will modify the internal keyboard focus of XEmacs
+      (select-window window))
+    buf))
+);;; End XEmacs only
+
+  
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;
 ;;; Old Emacs version compatibility
 ;;;
 
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 2ca5c428..5c1c5f87 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -561,7 +561,8 @@ If proof-show-debug-messages is nil, do nothing."
 	(proof-display-and-keep-buffer proof-response-buffer))))
 
 
-;;; A handy utility function used in the "Buffers" menu.
+;;; A handy utility function used in the "Buffers" menu, and throughout
+;; the code.
 (defun proof-switch-to-buffer (buf &optional noselect)
   "Switch to or display buffer BUF in other window unless already displayed.
 If optional arg NOSELECT is true, don't switch, only display it.
@@ -571,8 +572,12 @@ No action if BUF is nil or killed."
   (and (buffer-live-p buf)
        (unless (eq buf (window-buffer (selected-window)))
 	 (if noselect
-	     (display-buffer buf t)
-	   (switch-to-buffer-other-window buf)))))
+	     ;; FIXME: would like 'norecord arg here to override
+	     ;; previous window entering top of MRU list here.
+	     (display-buffer buf 'not-this-window)
+	   (let ((pop-up-windows t))
+	     (pg-pop-to-buffer buffer 'not-this-window 'norecord))))))  
+  
 
 ;; Originally based on `shrink-window-if-larger-than-buffer', which
 ;; has a pretty wierd implementation.