Overhaul and fixes for display management.

3 files changed, 294 insertions, 157 deletions

diff --git a/generic/pg-response.el b/generic/pg-response.el
index b566a1c1..7dfcb299 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -1,6 +1,6 @@
 ;; pg-response.el  Proof General response buffer mode.
 ;;
-;; Copyright (C) 1994-2002 LFCS Edinburgh. 
+;; Copyright (C) 1994-2004 LFCS Edinburgh. 
 ;; Authors:   David Aspinall, Healfdene Goguen, 
 ;;		Thomas Kleymann and Dilip Sequeira
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
@@ -52,54 +52,152 @@
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; 
-;; Multiple frames for goals and response buffers
-;;
-;;  -- because who's going to bother do this by hand?
+;; Window configuration
+;;   -- multiple frames for goals and response buffers,
+;;   -- three window mode
 ;;
 
 (defvar proof-shell-special-display-regexp nil
   "Regexp for special-display-regexps for multiple frame use.
 Internal variable, setting this will have no effect!")
 
+;; NB: this list uses XEmacs defaults in the non-multiframe case.
+;; We handle specifiers quit crudely, but (1) to set for the 
+;; frame specifically we'd need to get hold of the frame,
+;; (2) specifiers have been completely buggy.
+(defconst proof-multiframe-specifiers 
+;  (mapcar
+;   (lambda (spec) (list spec nil t)) ;; (specifier-specs spec)
+;     (list has-modeline-p menubar-visible-p 
+;	   default-gutter-visible-p default-toolbar))
+  (if proof-running-on-XEmacs
+      (list 
+       (list has-modeline-p nil nil) ;; nil even in ordinary case.
+       (list menubar-visible-p nil t)
+       (list default-gutter-visible-p nil t)
+       (list default-toolbar-visible-p nil t)))
+  "List of XEmacs specifiers and their values for non-multiframe and multiframe.")
+
+(defun proof-map-multiple-frame-specifiers (multiframep locale)
+  "Set XEmacs specifiers according to MULTIFRAMEP in LOCALE."
+  (dolist (spec proof-multiframe-specifiers)
+    (set-specifier (car spec) 
+		   (if multiframep (cadr spec) (caddr spec) )
+		   locale)))
+
+(defconst proof-multiframe-parameters
+  '((minibuffer . nil)
+    (unsplittable . t)
+    (menu-bar-lines . 0)
+    (tool-bar-lines . nil))
+  "List of GNU Emacs frame parameters for secondary frames.")
+
 (defun proof-multiple-frames-enable ()
+  ;; FIXME: add GNU Emacs version here.
+  ;; Try to trigger re-display of goals/response buffers,
+  ;; on next interaction.  
+  (if proof-running-on-XEmacs
+      (proof-map-buffers
+       (proof-associated-buffers)
+       (proof-map-multiple-frame-specifiers proof-multiple-frames-enable
+					    (current-buffer))))
+  (let ((spdres 
+	 (if proof-running-on-XEmacs
+	     proof-shell-special-display-regexp
+	   ;; GNU Emacs uses this to set frame params too, handily
+	   (cons 
+	    proof-shell-special-display-regexp
+	    proof-multiframe-parameters))))
+    (cond
+     (proof-multiple-frames-enable
+      (setq special-display-regexps
+	    (union special-display-regexps (list spdres))))
+     (t
+      (setq special-display-regexps
+	    (delete spdres special-display-regexps)))))
+  (proof-layout-windows))
+
+(defun proof-three-window-enable ()
+  (proof-layout-windows))
+
+
+(defun proof-select-three-b (b1 b2 b3)
+  "Select three buffers. Put them into three windows, selecting the last one."
+  (interactive "bBuffer1:\nbBuffer2:\nbBuffer3:")
+  (delete-other-windows)
+  (split-window-horizontally)
+  (switch-to-buffer b1)
+  (other-window 1)
+  (split-window-vertically)
+  (switch-to-buffer b2)
+  (other-window 1)
+  (switch-to-buffer b3)
+  (other-window 1))
+
+(defun proof-display-three-b ()
+  "Layout three buffers in a single frame."
+  (interactive)
+  (proof-select-three-b
+   (or proof-script-buffer (first (buffer-list)))
+   ;; Pierre had response buffer first, I think goals
+   ;; is a bit nicer though?
+   (if (buffer-live-p proof-goals-buffer) 
+       proof-goals-buffer (first (buffer-list)))
+   (if (buffer-live-p proof-response-buffer) 
+       proof-response-buffer (first (buffer-list)))))
+
+(defvar pg-frame-configuration nil
+  "Variable storing last used frame configuration.")
+
+;; FIXME: would be nice to try storing this persistently.
+(defun pg-cache-frame-configuration ()
+  "Cache the current frame configuration, between prover restarts."
+  (setq pg-frame-configuration (current-frame-configuration)))
+
+(defun proof-layout-windows ()
+  "Refresh the display of windows according to current display mode.
+This uses a canonical layout."
+  (interactive)
   (cond
    (proof-multiple-frames-enable
-    (setq special-display-regexps
-	  (union special-display-regexps 
-		 (list proof-shell-special-display-regexp)))
-    ;; If we're on XEmacs with toolbar, turn off toolbar and
-    ;; menubar for the small frames to save space.
-    ;; FIXME: this could be implemented more smoothly
-    ;; with property lists, and specifiers should perhaps be set
-    ;; for the frame rather than the buffer.  Then could disable
-    ;; minibuffer, too.
-    ;; FIXME: add GNU Emacs version here.
-    (if (featurep 'toolbar) 
-	(proof-map-buffers
-	 (list proof-response-buffer proof-goals-buffer proof-trace-buffer)
-	 (set-specifier default-toolbar-visible-p nil (current-buffer))
-	 ; (set-specifier minibuffer (minibuffer-window) (current-buffer))
-	 ;(set-specifier has-modeline-p nil (current-buffer))
-	 (remove-specifier has-modeline-p (current-buffer))
-	 (remove-specifier menubar-visible-p (current-buffer))
-	 ;; gutter controls buffer tab visibility in XE 21.4
-	 (and (boundp 'default-gutter-visible-p)
-	      (remove-specifier default-gutter-visible-p (current-buffer)))))
-    ;; Try to trigger re-display of goals/response buffers,
-    ;; on next interaction.  
-    ;; FIXME: would be nice to do the re-display here, rather
-    ;; than waiting for next re-display
-    (delete-other-windows 
-     (if proof-script-buffer
-	 (get-buffer-window proof-script-buffer t))))
+    (delete-other-windows) ;; hope we're on the right frame/window
+    (if proof-script-buffer
+	(switch-to-buffer proof-script-buffer))
+    (proof-map-buffers (proof-associated-buffers)
+      (proof-display-and-keep-buffer (current-buffer)))
+    ;; Restore an existing frame configuration (seems buggy, typical)
+    (if pg-frame-configuration
+	(set-frame-configuration pg-frame-configuration 'nodelete)))
+   ;; Three window mode: use the Pierre-layout by default
+   (proof-three-window-enable
+    (proof-delete-other-frames)
+    (proof-display-three-b))
+   ;; Two-of-three window mode.  
+   ;; Show the response buffer as first in preference order.
    (t
-    ;; FIXME: would be nice to kill off frames automatically,
-    ;; but let's leave it to the user for now.
-    (setq special-display-regexps
-	  (delete proof-shell-special-display-regexp 
-		  special-display-regexps)))))
-
-
+    (proof-delete-other-frames)
+    (delete-other-windows)
+    (if (buffer-live-p proof-response-buffer)
+	(proof-display-and-keep-buffer proof-response-buffer)))))
+
+(defun proof-delete-other-frames ()
+  "Delete frames showing associated buffers."
+  (save-selected-window
+    ;; FIXME: this is a bit too brutal.  If there is no
+    ;; frame for the associated buffer, we may delete
+    ;; the main frame!!
+    (let ((mainframe
+	   (window-frame 
+	    (if proof-script-buffer
+		(proof-get-window-for-buffer proof-script-buffer)
+	      ;; We may lose with just selected window
+	      (selected-window)))))
+      (proof-map-buffers (proof-associated-buffers)
+	(let ((fm (window-frame
+		   (proof-get-window-for-buffer (current-buffer)))))
+	  (unless (equal mainframe fm)
+	    (delete-frame fm)))))))
+	
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; 
 ;; Displaying in the response buffer
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index ea700deb..35fca76d 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -23,7 +23,9 @@
 A fixed number of repetitions of this command switches back to
 the same buffer.
 Also move point to the end of the response buffer if it's selected.
-If in three window or multiple frame mode, display two buffers."
+If in three window or multiple frame mode, display two buffers.
+The idea of this function is to change the window->buffer mapping 
+without adjusting window layout."
   (interactive)
   ;; The GUI-tessence here is to implement a humane toggle, which
   ;; allows habituation.  E.g. two taps of C-c C-l always
@@ -38,30 +40,36 @@ If in three window or multiple frame mode, display two buffers."
    (t
     (setq proof-display-some-buffers-count 0)))
   (let* ((assocbufs   (remove-if-not 'buffer-live-p 
-				    (list proof-response-buffer
-					  proof-thms-buffer
-					  proof-trace-buffer
-					  proof-goals-buffer
-					  )))
+				     (list proof-response-buffer
+					   proof-thms-buffer
+					   proof-trace-buffer
+					   proof-goals-buffer
+					   )))
 					;proof-shell-buffer
-	 (selectedbuf (nth (mod proof-display-some-buffers-count 
-				(length assocbufs)) assocbufs))
-	 (nextbuf     (nth (mod (1+ proof-display-some-buffers-count)
-				(length assocbufs)) assocbufs)))
-    (cond
-     ((or proof-three-window-mode proof-multiple-frames-enable)
-      ;; Display two buffers: next in rotation and goals/response
-      ;; FIXME: this doesn't work as well as it might.
-      (proof-switch-to-buffer selectedbuf 'noselect)
-      (proof-switch-to-buffer (if (eq selectedbuf proof-goals-buffer)
-				  proof-response-buffer
-				proof-goals-buffer) 'noselect))
-     (selectedbuf
-      (proof-switch-to-buffer selectedbuf 'noselect)))
-    (if (eq selectedbuf proof-response-buffer)
-	(set-window-point (get-buffer-window proof-response-buffer)
-			  (point-max)))
-    (pg-hint (pg-response-buffers-hint (buffer-name nextbuf)))))
+	 (numassoc    (length assocbufs)))
+    ;; If there's no live other buffers, we don't do anything.
+    (unless (zerop numassoc)
+      (let
+	 ((selectedbuf (nth (mod proof-display-some-buffers-count 
+				 numassoc) assocbufs))
+	  (nextbuf     (nth (mod (1+ proof-display-some-buffers-count)
+				 numassoc) assocbufs)))
+	(cond
+	 ((or proof-three-window-enable proof-multiple-frames-enable)
+	  ;; Display two buffers: next in rotation and goals/response
+	  ;; FIXME: this doesn't work as well as it might.
+	  (proof-switch-to-buffer selectedbuf 'noselect)
+	  (proof-switch-to-buffer (if (eq selectedbuf proof-goals-buffer)
+				      proof-response-buffer
+				    proof-goals-buffer) 'noselect))
+	 (selectedbuf
+	  (proof-switch-to-buffer selectedbuf 'noselect)))
+	(if (eq selectedbuf proof-response-buffer)
+	    (set-window-point (get-buffer-window proof-response-buffer t)
+			      (point-max)))
+	(unless (or proof-three-window-enable proof-multiple-frames-enable)
+	  ;; The hint only makes sense in two-window mode, really.
+	  (pg-hint (pg-response-buffers-hint (buffer-name nextbuf))))))))
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -84,7 +92,8 @@ If in three window or multiple frame mode, display two buffers."
 ;; C-c C-c is proof-interrupt-process in universal-keys
 (define-key map [(control c) (control f)] 'proof-find-theorems)
 (define-key map [(control c) (control h)] 'proof-help)
-(define-key map [(control c) (control l)] 'proof-display-some-buffers)
+(define-key map [(control c) (control o)] 'proof-display-some-buffers)
+(define-key map [(control c) (control l)] 'proof-layout-windows)
 (define-key map [(control c) (control n)] 'proof-assert-next-command-interactive)
 (define-key map [(control c) (control p)] 'proof-prf)
 (define-key map [(control c) (control r)] 'proof-retract-buffer)
@@ -198,19 +207,21 @@ If in three window or multiple frame mode, display two buffers."
   "Proof General help menu.")
 
 (defvar proof-show-hide-menu
-  '(("Show all"
+  '(("Show All"
      ["Proofs"    (pg-show-all-portions "proof") t]
      ["Comments"  (pg-show-all-portions "comment") t])
-    ("Hide all"
+    ("Hide All"
      ["Proofs"    (pg-show-all-portions "proof" 'hide) t]
      ["Comments"  (pg-show-all-portions "comment" 'hide) t]))
   "Show/hide submenu.")
 
 (defvar proof-buffer-menu
   (cons "Buffers"
-	'(["Active Scripting"
-	    (proof-switch-to-buffer proof-script-buffer)
-	    :active (buffer-live-p proof-script-buffer)]
+	'(;;["Active Scripting"
+	  ;;  (proof-switch-to-buffer proof-script-buffer)
+	  ;;  :active (buffer-live-p proof-script-buffer)]
+	   ["Layout Windows"
+	    proof-layout-windows]
 	   ["Rotate Output Buffers"
 	    proof-display-some-buffers
 	    :active (buffer-live-p proof-goals-buffer)]
@@ -220,7 +231,7 @@ If in three window or multiple frame mode, display two buffers."
 	   ;;["Response"
 	   ;; (proof-switch-to-buffer proof-response-buffer t)
 	   ;; :active (buffer-live-p proof-response-buffer)]
-	   ["Shell"
+	   ["Show Shell"
 	    (proof-switch-to-buffer proof-shell-buffer)
 	    :active (buffer-live-p proof-shell-buffer)]
 	   ;; FIXME: this next test doesn't work since menus
@@ -244,11 +255,11 @@ If in three window or multiple frame mode, display two buffers."
 
 ;; First, make the togglers used in options menu below
 
-(proof-deftoggle proof-three-window-mode)
 (proof-deftoggle proof-script-fly-past-comments)
 (proof-deftoggle proof-delete-empty-windows)
 (proof-deftoggle proof-shrink-windows-tofit)
 (proof-deftoggle proof-multiple-frames-enable proof-multiple-frames-toggle)
+(proof-deftoggle proof-three-window-enable proof-three-window-toggle)
 ;; (proof-deftoggle proof-output-fontify-enable proof-output-fontify-toggle)
 (proof-deftoggle proof-disappearing-proofs)
 (proof-deftoggle proof-strict-read-only)
@@ -304,22 +315,25 @@ If in three window or multiple frame mode, display two buffers."
       :style toggle
       :selected proof-toolbar-enable]
      ("Display"
-      ["Three Window Mode" proof-three-window-mode-toggle
+      ["Use Three Panes" proof-three-window-toggle
        :active (not proof-multiple-frames-enable)
        :style toggle
-       :selected proof-three-window-mode]
-      ["Delete Empty Windows" proof-delete-empty-windows-toggle
+       :selected proof-three-window-enable]
+      ;; We use non-Emacs terminology "Windows" in this menu to help
+      ;; non-Emacs users.  Cf. Gnome usability studies: menus saying
+      ;; "Web Browser" more useful to novices than menus saying "Mozilla"!!
+      ["Multiple Windows" proof-multiple-frames-toggle
+       :active (display-graphic-p)
+       :style toggle
+       :selected proof-multiple-frames-enable]
+      ["Delete Empty Panes" proof-delete-empty-windows-toggle
        :active (not proof-multiple-frames-enable)
        :style toggle
        :selected proof-delete-empty-windows]
       ["Shrink to Fit" proof-shrink-windows-tofit-toggle
        :active (not proof-multiple-frames-enable)
        :style toggle
-       :selected proof-shrink-windows-tofit]
-      ["Multiple Frames" proof-multiple-frames-toggle
-       :active (display-graphic-p)
-       :style toggle
-       :selected proof-multiple-frames-enable])
+       :selected proof-shrink-windows-tofit])
      ("Follow Mode" 
       ["Follow Locked Region" 
        (customize-set-variable 'proof-follow-mode 'locked)
@@ -370,7 +384,7 @@ If in three window or multiple frame mode, display two buffers."
    (proof-ass-sym mmm-enable)
    'proof-toolbar-enable
    ;; Display sub-menu
-   'proof-three-window-mode
+   'proof-three-window-enable
    'proof-delete-empty-windows
    'proof-multiple-frames-enable
    'proof-shrink-windows-tofit
@@ -795,20 +809,12 @@ evaluate can be provided instead."
 
 
 (defun proof-assistant-settings-cmd (&optional setting)
-  "Return string for making setting vals kept in Proof General customizations.
+  "Return string for settings kept in Proof General customizations.
 If SETTING is non-nil, return a string for just that setting. 
 Otherwise return a string for configuring all settings.
 
-If `proof-assistants-settings' is nil and PGIP is supported, then
+If `proof-assistant-settings' is nil and PGIP is supported, then
 first we query settings information from prover."
-  ;; This is a slightly ugly way: this function may be called to
-  ;; calculate a string for setting preferences, and is a possible
-  ;; setting for proof-shell-init-cmd.  But it needs to be evaluated
-  ;; each time (in case preferences change), and may trigger a nested
-  ;; call to proof-shell-invisible-cmd to send askprefs message.
-  (if (and (not proof-assistant-settings)
-	   proof-shell-issue-pgip-cmd)
-      (pg-pgip-askprefs))
   (let
       ((evalifneeded (lambda (expr)
 			(if (and (cadr expr) ;; setting has PA string?
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index dab732e2..8df5455a 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -467,27 +467,23 @@ Default to whole buffer.  Leave point at END."
   (unless (and (boundp sym) (symbol-value sym))
     (warn "Proof General %s: %s is unset."  tag (symbol-name sym))))
 
-(defun proof-display-and-keep-buffer (buffer &optional pos)
-  "Display BUFFER and mark window according to `proof-three-window-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."
-  (let (window)
-    (save-excursion
-      (save-selected-window
-	(set-buffer buffer)
-	(if (and 
+(defun proof-get-window-for-buffer (buffer)
+  "Find a window for BUFFER, display it there, return the window.
+NB: may change the selected window."
+  ;; IF there *isn't* a visible window showing buffer...
+  (unless (get-buffer-window buffer 'visible)
+    ;; THEN find somewhere nice to display it
+	  (if (and 
 	     ;; If we're in two-window mode and already displaying a
 	     ;; script/response/goals, try to just switch the buffer
 	     ;; instead of calling display-buffer which alters sizes.
 	     ;; Gives user some stability on display.
-	     (not proof-three-window-mode)
+	     (not proof-three-window-enable)
 	     (> (count-windows) 1)
 	     ;; was: (not (eq (next-window) (selected-window)))
 	     (memq (window-buffer (next-window nil 'ignoreminibuf))
-		   (list proof-script-buffer 
-			 proof-response-buffer
-			 proof-goals-buffer)))
+		   ;; NB: 3.5: added rest of assoc'd buffers here
+		   (cons proof-script-buffer (proof-associated-buffers))))
 	    (if (eq (selected-window) (minibuffer-window))
 		;; 17.8.01: avoid switching the minibuffer's contents 
 		;; -- terrrible confusion -- use next-window after
@@ -498,33 +494,46 @@ Ensure that point is visible in window."
 		  (car-safe (get-buffer-window-list proof-script-buffer))
 		  'ignoreminibuf) buffer)
 	      (if (eq (window-buffer (next-window nil 'ignoreminibuf))
-		      proof-script-buffer)
+		      proof-script-buffer) 
 		  ;; switch this window
-		  (set-window-buffer (selected-window) buffer)
+		  (set-window-buffer (selected-window) buffer) 
 		;; switch other window
 		(set-window-buffer (next-window nil 'ignoreminibuf) buffer)))
 	  ;; o/w: call display buffer to configure windows nicely.
-	  (display-buffer buffer))
-	;; Suggestion: cache previous height of other window to attempt
-	;; to regenerate the display as the user last had it.
-	(setq window (get-buffer-window buffer 'visible))
-	(if (window-live-p window) ;; fails sometimes, don't know why
-	  (progn
-	    (set-window-dedicated-p window proof-three-window-mode)
-	    (select-window window)
-	    (if proof-shrink-windows-tofit
-		(proof-resize-window-tofit))
-	    ;; For various reasons, point may get moved around in
-	    ;; response buffer.  Attempt to normalise its position.
-	    (goto-char (or pos (point-max)))
-	    (if pos 
-		(beginning-of-line)
-	      (skip-chars-backward "\n\t "))
-	    ;; Ensure point visible.  Again, window may have died
-	    ;; inside shrink to fit, for some reason
-	    (if (window-live-p window) 
-		(unless (pos-visible-in-window-p (point) window)
-		  (recenter -1)))))))))
+	    (display-buffer buffer)))
+  ;; Return the window, hopefully the one we first thought of.
+  (get-buffer-window buffer 'visible))
+
+(defun proof-display-and-keep-buffer (buffer &optional pos)
+  "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
+    (save-selected-window
+      (let ((window (proof-get-window-for-buffer buffer)))
+	(if (window-live-p window) ;; [fails sometimes?]
+	    (progn
+	      ;; Set the size and point position.
+	      (set-window-dedicated-p window proof-three-window-enable)
+	      (select-window window)
+	      (if proof-shrink-windows-tofit
+		  (proof-resize-window-tofit)
+		;; If we're not shrinking to fit, allow the size of
+		;; this window to change.  [NB: might be nicer to
+		;; fix the size based on user choice]
+		(setq window-size-fixed nil))
+	      ;; For various reasons, point may get moved around in
+	      ;; response buffer.  Attempt to normalise its position.
+	      (goto-char (or pos (point-max)))
+	      (if pos 
+		  (beginning-of-line)
+		(skip-chars-backward "\n\t "))
+	      ;; Ensure point visible.  Again, window may have died
+	      ;; inside shrink to fit, for some reason
+	      (if (window-live-p window) 
+		  (unless (pos-visible-in-window-p (point) window)
+		    (recenter -1)))))))))
 
 (defun proof-clean-buffer (buffer)
   "Erase buffer and hide from display if proof-delete-empty-windows set.
@@ -585,9 +594,17 @@ No action if BUF is nil or killed."
 
 ;; Originally based on `shrink-window-if-larger-than-buffer', which
 ;; has a pretty wierd implementation.
-;; FIXME: desirable improvements would be to add some crafty history based
+;; TODO: desirable improvements would be to add some crafty history based
 ;; on user resize-events.  E.g. user resizes window, that becomes the 
 ;; new maximum size.
+;; FIXME: GNU Emacs has useful "window-size-fixed" which we use
+;; HOWEVER, it's still not quite the right thing, it seems to me.
+;; We'd like to specifiy a *minimum size* for a given buffer, 
+;; not a maximum.  With a frame split with just goals/response
+;; we'd still get resize errors here using window-size-fixed.
+;; FIXME: shrink-to-fit doesn't really work in three-buffer mode,
+;; since shrinking one of the associated buffers tends to enlarge the
+;; other (rather than just enlarging the proof state)
 (defun proof-resize-window-tofit (&optional window)
   "Shrink the WINDOW to be as small as possible to display its contents.
 Do not shrink to less than `window-min-height' lines.
@@ -595,14 +612,15 @@ Do nothing if the buffer contains more lines than the present window height,
 or if some of the window's contents are scrolled out of view,
 or if the window is not the full width of the frame,
 or if the window is the only window of its frame."
+;; da: actually seems okay in this case
   (interactive)
   (or window (setq window (selected-window)))
   ;; some checks before resizing to avoid messing custom display
   ;; [probably somewhat superfluous/extra rare]
-  (unless 
+  (if 
       (or
        ;; The frame must not be minibuffer-only.
-       (eq (frame-property (window-frame window) 'minibuffer) 'only)
+       (eq (frame-parameter (window-frame window) 'minibuffer) 'only)
        ;; We've got more than one window, right?
        (= 1 (let ((frame (selected-frame)))
 	      (select-frame (window-frame window))
@@ -611,18 +629,28 @@ or if the window is the only window of its frame."
 		(select-frame frame)
 		(select-window window))))
        ;; the window is the full width, right?
+       ;; [if not, we may be in horiz-split scheme, problematic]
        (not (window-leftmost-p window))
        (not (window-rightmost-p window)))
+      ;; OK, we're not going to adjust the height here.  Moreover,
+      ;; we'll make sure the height can be changed elsewhere.
+      (setq window-size-fixed nil)
     (save-excursion
       (set-buffer (window-buffer window))
       (let* 
 	  ;; weird test cases:
 	  ;; cur=45, max=23, desired=121, extraline=0
 	  ;; current height
-	  ((cur-height (window-height window))
+	  ;;; ((cur-height (window-height window))
 	   ;; Most window is allowed to grow to
-	   (max-height  (/ (frame-height (window-frame window)) 
-			   (if proof-three-window-mode 3 2)))
+	  ((max-height  
+	    (/ (frame-height (window-frame window)) 
+	       (if proof-three-window-enable 
+		   ;; we're in three-window-mode with
+		   ;; all horizontal splits, so share the height.
+		   3
+		 ;; Otherwise assume a half-and-half split
+		 2)))
 	   ;; If buffer ends with a newline, ignore it when counting
 	   ;; height unless point is after it.
 	   (extraline 
@@ -633,39 +661,43 @@ or if the window is the only window of its frame."
 	   ;; Direction of resizing based on whether max position is 
 	   ;; currently visible.  [ FIXME: not completely sensible:
 	   ;; may be displaying end fraction of buffer! ]
-	   (shrink (pos-visible-in-window-p test-pos window))
+	   ;; (shrink (pos-visible-in-window-p test-pos window))
 	   ;; Likely desirable height is given by count-lines
 	   (desired-height 
 	    ;; FIXME: is count-lines too expensive for v.large
 	    ;; buffers?  Probably not an issue for us, but one
 	    ;; wonders at the shrink to fit strategy.
 	    ;; NB: way to calculate pixel fraction?
-	    (+ extraline 2 (count-lines (point-min) (point-max)))))
-	;; 
-	;; Let's shrink or expand
-	(cond
-	 ((and shrink
-	       (> cur-height window-min-height)
-	       ;; don't shrink if already too big; leave where it is
-	       (< cur-height max-height))
-	  (shrink-window 
-	   (- cur-height (max window-min-height desired-height))
-	   nil window))
-	 (;; expand
-	  (< cur-height max-height)
-	  (enlarge-window 
-	   (- (min max-height desired-height) cur-height) 
-	   nil window)))
+	    (+ extraline 1 (count-lines (point-min) (point-max)))))
+	;; Let's shrink or expand.  Uses new GNU Emacs function.
+	(let ((window-size-fixed nil))
+	  (set-window-text-height window desired-height))
+;; 	(cond
+;; 	 ((and shrink
+;; 	       (> cur-height window-min-height)
+;; 	       ;; don't shrink if already too big; leave where it is
+;; 	       (< cur-height max-height))
+;; 	  (with-selected-window 
+;; 	   window
+;; 	   (shrink-window (- cur-height (max window-min-height desired-height)))))
+;; 	 (;; expand
+;; 	  (< cur-height max-height)
+;; 	  (with-selected-window window
+;; 	   (enlarge-window 
+;; 	    (- (min max-height desired-height) cur-height)))))
 	;; If we're at least the desirable height, it must be that the
 	;; whole buffer can be seen --- so make sure display starts at
 	;; beginning.
-	;; FIXME: problem here, get errors that the window is
-	;; no longer live!!  (Does it change reference after
-	;; resizing???  Or are we calling this function
-	;; with a dead window?)
+	;; NB: shrinking windows can sometimes delete them
+	;; (although we don't want it to here!), but make this next 
+	;; check for robustness.
 	(if (window-live-p window)
-	    (if (>= (window-height window) desired-height)
-		(set-window-start window (point-min))))))))
+	    (progn
+	      (if (>= (window-height window) desired-height)
+		  (set-window-start window (point-min)))
+	      ;; window-size-fixed is a GNU Emacs buffer local variable 
+	      ;; which determines window size of buffer.
+	      (setq window-size-fixed (window-height window))))))))
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -826,6 +858,7 @@ EXTRAPATH is a list of extra path components"
 (put 'proof-define-assistant-command 'lisp-indent-function 'defun)
 (put 'proof-define-assistant-command-witharg 'lisp-indent-function 'defun)
 (put 'defpgcustom 'lisp-indent-function 'defun)
+(put 'proof-map-buffers 'lisp-indent-function 'defun)
 
 (defconst proof-extra-fls
   (list
@@ -844,7 +877,7 @@ EXTRAPATH is a list of extra path components"
        nil t)))
 
 ;; This doesn't work for FSF's font lock, developers should use
-;; XEmacs!
+;; XEmacs!  (unless edebug is broken, which it is in my 21.4.12)
 (if (boundp 'lisp-font-lock-keywords)	; compatibility hack
     (setq lisp-font-lock-keywords 
 	  (append proof-extra-fls