Experimenting smarter window creation when in three windows

mode. Strategy is: always try to split an associated buffer window.

2 files changed, 34 insertions, 2 deletions

diff --git a/generic/pg-assoc.el b/generic/pg-assoc.el
index ba987aeb..deb40e56 100644
--- a/generic/pg-assoc.el
+++ b/generic/pg-assoc.el
@@ -38,6 +38,14 @@ Some may be dead/nil."
 	proof-thms-buffer))
 
 
+(defun proof-associated-windows ()
+  "Return a list of the associated buffers windows.  
+dead or nil buffers are not represented in the list."
+  (let ((lwin (mapcar '(lambda (b) (and b (get-buffer-window b))) 
+		     (proof-associated-buffers))))
+    (proof-list-filter lwin '(lambda (x) (not (null x))))
+    ))
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Manipulating prover output
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index dc230872..1bdf12bc 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -59,6 +59,16 @@ Return nil if not a script buffer or if no active scripting buffer."
     (file-error nil))
   (featurep symbol))
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Handy functions ; should perhaps be elsewhere ?
+
+(defun proof-list-filter (l test)
+  "Build a list containing elements of L satifying predicate test."
+  (if (null l) nil 
+    (if (funcall test (car l)) (cons (car l) (proof-list-filter (cdr l) test))
+      (proof-list-filter (cdr l) test))))
+
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -527,8 +537,22 @@ NB: may change the selected window."
 		  (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)))
+	    ;; o/w: call display buffer to configure windows nicely.
+	    ;; PC: Experimental this was simply (display-buffer buffer) but I am
+	    ;; experimenting the following policy: when in three windows
+	    ;; mode, always make new windo on the right pane, that is:
+	    ;; always split one of the associated buffers windows
+	    ;; this is not perfect, let's see if people like it
+	    (let ((associated-windows (proof-associated-windows)))
+	      (if (not (and proof-three-window-enable associated-windows))
+		  (display-buffer buffer)
+		(select-window (car associated-windows)) ; take on assoc. win
+		(split-window-vertically)
+		(set-window-dedicated-p (selected-window) nil)
+		(switch-to-buffer buffer)
+		(set-window-dedicated-p (selected-window) t)
+		))
+	    ))
   ;; Return the window, hopefully the one we first thought of.
   (get-buffer-window buffer 0))