Fixed a compilation issue + small display glitch in coqpg

2 files changed, 48 insertions, 8 deletions

diff --git a/generic/pg-response.el b/generic/pg-response.el
index 009c6492..1c005998 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -114,7 +114,7 @@ Internal variable, setting this will have no effect!")
 	((display-buffer-entry
 	  (cons pg-response-special-display-regexp
 	    `((display-buffer-reuse-window display-buffer-pop-up-frame) .
-	      ((reusable-frames . nil)
+	      ((reusable-frames . t)
 	       (pop-up-frame-parameters
 		.
 		,proof-multiframe-parameters))))))
@@ -235,22 +235,29 @@ dragging the separating bars.
   (interactive)
   (cond
    (proof-multiple-frames-enable
+    ;; If we are coming from single frame mode, delete associated
+    ;; windows (and only them).
     (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)
-      (if pg-response-eagerly-raise
-	  (proof-display-and-keep-buffer (current-buffer) nil 'force)))
+    (proof-map-buffers
+     (proof-associated-buffers)
+     (if pg-response-eagerly-raise
+	 (proof-display-and-keep-buffer (current-buffer) nil 'force)))
     ;; Restore an existing frame configuration (seems buggy, typical)
     (if pg-frame-configuration
 	(set-frame-configuration pg-frame-configuration 'nodelete)))
-   (proof-three-window-enable
+   (proof-three-window-enable ; single frame
+    ;; If we are coming from multiple frame mode, delete associated
+    ;; frames (and only them).
     (proof-delete-other-frames)
     (set-window-dedicated-p (selected-window) nil)
     (proof-display-three-b proof-three-window-mode-policy))
    ;; Two-of-three window mode.
    ;; Show the response buffer as first in preference order.
    (t
+    ;; If we are coming from multiple frame mode, delete associated
+    ;; frames (and only them).
     (proof-delete-other-frames)
     (set-window-dedicated-p (selected-window) nil)
     (delete-other-windows)
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index a88c3e08..d4e0f803 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -243,10 +243,43 @@ without adjusting window layout."
      ["Comments"   (pg-show-all-portions 'comment 'hide) t]))
   "Show/hide submenu.")
 
+
+(defvar proof-3-window-mode-policy
+  (cons "3 Windows mode layout"
+	'(["smart"
+	   (progn
+	     (customize-set-variable 'proof-three-window-mode-policy 'smart)
+	     (proof-layout-windows))
+	   :style radio
+	   :selected (eq proof-three-window-mode-policy 'smart)
+	   :help "Adapt to frame width (C-c C-l to refresh)"]
+	  ["hybrid"
+	   (progn
+	     (customize-set-variable 'proof-three-window-mode-policy 'hybrid)
+	     (proof-layout-windows))
+	   :style radio
+	   :selected (eq proof-three-window-mode-policy 'hybrid)
+	   :help "two column mode"]
+	  ["horizontal"
+	   (progn
+	     (customize-set-variable 'proof-three-window-mode-policy 'horizontal)
+	     (proof-layout-windows))
+	   :style radio
+	   :selected (eq proof-three-window-mode-policy 'horizontal)
+	   :help "Three column mode"]
+	  ["vertical"
+	   (progn
+	     (customize-set-variable 'proof-three-window-mode-policy 'vertical)
+	     (proof-layout-windows))
+	   :style radio
+	   :selected (eq proof-three-window-mode-policy 'vertical)
+	   :help "One column mode"])))
+
 (defvar proof-buffer-menu
   (cons "Buffers"
-	'(["Layout Windows"
-	   proof-layout-windows]
+	`(["Layout Windows" proof-layout-windows]
+	  ,proof-3-window-mode-policy
+	  ""
 	  ["Rotate Output Buffers"
 	   proof-display-some-buffers
 	   :visible (not proof-three-window-enable)
@@ -271,7 +304,7 @@ without adjusting window layout."
 	  ["Shell"
 	   (proof-switch-to-buffer proof-shell-buffer)
 	   :active (buffer-live-p proof-shell-buffer)]))
-  "Proof General buffer menu.")
+  "Proof General 3 window mode policy.")
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;