diff options
| author | David Aspinall | 1998-11-03 14:37:27 +0000 |
|---|---|---|
| committer | David Aspinall | 1998-11-03 14:37:27 +0000 |
| commit | d36aa837d21c8323b1bbe4fcf4f34f9688122018 (patch) | |
| tree | 65460021e7809abb12e3ae09cffa738fb0d1f37a | |
| parent | 34ddb5bbb486a9d23c6b567c5c7168847b673600 (diff) | |
Promoted proof-window-dedicated to be a user option, and
renamed it [to reserve -p only for functions (predicates)].
| -rw-r--r-- | generic/proof-config.el | 13 | ||||
| -rw-r--r-- | 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) |