Trying to not delete frames too eagerly when laying out.

3 files changed, 32 insertions, 4 deletions

diff --git a/generic/pg-assoc.el b/generic/pg-assoc.el
index 7bb6146d..7b983bbf 100644
--- a/generic/pg-assoc.el
+++ b/generic/pg-assoc.el
@@ -52,5 +52,22 @@ Dead or nil buffers are not represented in the list."
       (setq bufs (cdr bufs)))
     wins))
 
+
+(defun proof-associated-buffer-p (b) (member b (proof-associated-buffers)))
+
+
+(defun proof-filter-associated-windows (lw)
+  "Remove windows of LW not displaying at least one associated buffer."
+  (remove-if-not (lambda (w) (proof-associated-buffer-p (window-buffer w))) lw))
+
+(defun proof-find-all-associated-windows ()
+  "Return the list of windows displaying an associated buffer."
+  (proof-filter-associated-windows (window-list-1 nil nil t)))
+
+(defun proof-find-all-associated-frames ()
+  "Return the list of frames displaying at least one associated buffer."
+  (remove-if-not (lambda (f) (proof-filter-associated-windows (window-list f)))
+		 (frame-list)))
+
 (provide 'pg-assoc)
 ;;; pg-assoc.el ends here
diff --git a/generic/pg-response.el b/generic/pg-response.el
index 1c005998..e278cec3 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -184,6 +184,18 @@ Following POLICY, which can be one of 'smart, 'horizontal,
        proof-script-buffer proof-goals-buffer proof-response-buffer
        policy))))
 
+
+(defun proof-delete-all-associated-windows ()
+  "Delete windows (and maybe frames) showing associated buffers.
+Delete a frame if it displays only associated buffers, unless it
+is the only frame (try to bury buffers then)."
+  (mapc (lambda (w)
+	  ;; try to delete window, or frame, or only bury buffer
+	  (if (not (frame-root-window-p w)) (delete-window w)
+	    (if (< 1 (length (frame-list))) (delete-frame (window-frame w))
+	      (window--display-buffer (other-buffer) w 'window))))
+	(proof-find-all-associated-windows)))
+
 (defvar pg-frame-configuration nil
   "Variable storing last used frame configuration.")
 
@@ -250,7 +262,7 @@ dragging the separating bars.
    (proof-three-window-enable ; single frame
     ;; If we are coming from multiple frame mode, delete associated
     ;; frames (and only them).
-    (proof-delete-other-frames)
+    (proof-delete-all-associated-windows)
     (set-window-dedicated-p (selected-window) nil)
     (proof-display-three-b proof-three-window-mode-policy))
    ;; Two-of-three window mode.
@@ -258,9 +270,8 @@ dragging the separating bars.
    (t
     ;; If we are coming from multiple frame mode, delete associated
     ;; frames (and only them).
-    (proof-delete-other-frames)
+    (proof-delete-all-associated-windows)
     (set-window-dedicated-p (selected-window) nil)
-    (delete-other-windows)
     (if (buffer-live-p proof-response-buffer)
 	(proof-display-and-keep-buffer proof-response-buffer nil 'force))))
   (pg-hint (pg-response-buffers-hint)))
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 69af75f5..cb9ed2bb 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -491,7 +491,7 @@ shell buffer, called by `proof-shell-bail-out' if process exits."
     ;; frames (NB: loses if user has switched buffer in special frame)
     (if (and proof-multiple-frames-enable
 	     proof-shell-fiddle-frames)
-	(proof-delete-other-frames))
+	(proof-delete-all-associated-windows))
 
     ;; Kill associated buffer
     (let ((proof-shell-buffer nil)) ;; fool kill buffer hooks