From d36aa837d21c8323b1bbe4fcf4f34f9688122018 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 3 Nov 1998 14:37:27 +0000
Subject: Promoted proof-window-dedicated to be a user option, and renamed it
 [to reserve -p only for functions (predicates)].

---
 generic/proof-config.el | 13 ++++++++-----
 generic/proof.el        |  9 ++++-----
 2 files changed, 12 insertions(+), 10 deletions(-)

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 8d484171..3c90d5e9 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -71,6 +71,14 @@ If ignore, point is never moved after toolbar movement commands."
 	  (const :tag "Never move" ignore))
   :group 'proof-general)
 
+(defcustom proof-window-dedicated t
+  "*Whether response and goals buffers have dedicated windows.
+If t, windows displaying responses from the prover will not
+be switchable to display other windows.  This helps manage
+your display, but can sometimes be inconvenient, especially
+for experienced Emacs users."
+  :type 'boolean
+  :group 'proof-general)
 
 ;;
 ;; Faces.
@@ -702,11 +710,6 @@ where `k' is a keybinding (vector) and `f' the designated function."
   :type 'sexp
   :group 'proof-general-internals)
 
-(defcustom proof-window-dedicated-p t
-  "Flag whether response and goals buffers have dedicated windows."
-  :type 'boolean
-  :group 'proof-general-internals)
-
 ;;; 
 ;;; FIXME: unsorted below here
 ;;;
diff --git a/generic/proof.el b/generic/proof.el
index ef3e68a6..cdc3b5a5 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -52,9 +52,8 @@
 (autoload 'proof-shell-mode "proof-shell"
   "Proof General shell mode class for proof assistant processes")
 
-(if (featurep 'toolbar)
-    (autoload 'proof-toolbar-setup "proof-toolbar"
-      "Initialize Proof General and enable it for the current buffer" t))
+(autoload 'proof-toolbar-setup "proof-toolbar"
+  "Initialize Proof General toolbar and enable it for the current buffer" t)
 
 ;;;
 ;;; More autoloads to help define interface between files
@@ -151,7 +150,7 @@ The argument KBL is a list of tuples (k . f) where `k' is a keybinding
 
 
 (defun proof-display-and-keep-buffer (buffer)
-  "Display BUFFER and mark window according to `proof-window-dedicated-p'.
+  "Display BUFFER and mark window according to `proof-window-dedicated'.
 
 Also ensures that point is visible."
   (let (window)
@@ -159,7 +158,7 @@ Also ensures that point is visible."
       (set-buffer buffer)
       (display-buffer buffer)
       (setq window (get-buffer-window buffer 'visible))
-      (set-window-dedicated-p window proof-window-dedicated-p)
+      (set-window-dedicated-p window proof-window-dedicated)
       (and window
 	   (save-selected-window
 	     (select-window window)
-- 
cgit v1.2.3