Add hint to C-c C-l; cleanup hints, add menu for C-c C-l

3 files changed, 12 insertions, 6 deletions

diff --git a/generic/pg-response.el b/generic/pg-response.el
index 7dfcb299..abfdd328 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -171,14 +171,17 @@ This uses a canonical layout."
    ;; Three window mode: use the Pierre-layout by default
    (proof-three-window-enable
     (proof-delete-other-frames)
+    (set-window-dedicated-p (selected-window) nil)
     (proof-display-three-b))
    ;; Two-of-three window mode.  
    ;; Show the response buffer as first in preference order.
    (t
     (proof-delete-other-frames)
+    (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)))))
+	(proof-display-and-keep-buffer proof-response-buffer))))
+  (pg-hint (pg-response-buffers-hint)))
 
 (defun proof-delete-other-frames ()
   "Delete frames showing associated buffers."
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 2c490569..c439e995 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -1023,8 +1023,11 @@ If NUM is negative, move upwards.  Return new span."
 (defun pg-response-buffers-hint (&optional nextbuf)
   (pg-hint
    (format
-    "Use \\[proof-prf] to display goals; \\[proof-display-some-buffers] to rotate output %s"
-    (if nextbuf (concat "(next: " nextbuf ")") ""))))
+    "\\[proof-prf] displays goals;%s \\[proof-layout-windows] refreshes"
+    (if (not proof-multiple-frames-enable) ;; and not proof-three-window-enable? 
+	(format " \\[proof-display-some-buffers] rotates output%s;"
+		(if nextbuf (concat " (next:" nextbuf ")") ""))
+      ""))))
 
 (defun pg-jump-to-end-hint ()
   (pg-hint "Use \\[proof-goto-end-of-locked] to jump to end of processed region"))
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 35fca76d..daa5bdc3 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -67,9 +67,8 @@ without adjusting window layout."
 	(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))))))))
+	(pg-hint (pg-response-buffers-hint (buffer-name nextbuf)))))))
+
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -315,6 +314,7 @@ without adjusting window layout."
       :style toggle
       :selected proof-toolbar-enable]
      ("Display"
+      ["Layout windows" proof-layout-windows]
       ["Use Three Panes" proof-three-window-toggle
        :active (not proof-multiple-frames-enable)
        :style toggle