diff options
| -rw-r--r-- | generic/pg-response.el | 8 | ||||
| -rw-r--r-- | generic/proof-useropts.el | 2 |
2 files changed, 6 insertions, 4 deletions
diff --git a/generic/pg-response.el b/generic/pg-response.el index d6bf8651..561436b0 100644 --- a/generic/pg-response.el +++ b/generic/pg-response.el @@ -160,9 +160,11 @@ Emacs windows vertically in equal proportions. You can then adjust the proportions by dragging the separating bars. In three pane mode, the canonical layout is to split both horizontally and vertically, to display the prover responses in two panes on the right-hand side, and -the proof script in a taller pane on the left. A prefix argument will -prevent the horizontal split, and result in three windows spanning the -full width of the Emacs frame. +the proof script in a taller pane on the left. However if +`proof-three-window-mode-policy' is set to 'smart (it is by default) +this layout will not be applied if the width of the frame is too small, +and result in three windows spanning the full width of the Emacs frame. +See `proof-three-window-mode-policy' for other splitting policy. For multiple frame mode, this function obeys the setting of `pg-response-eagerly-raise', which see." diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el index e6712ff6..d023a67e 100644 --- a/generic/proof-useropts.el +++ b/generic/proof-useropts.el @@ -139,7 +139,7 @@ you a reprimand!)." :set 'proof-set-value :group 'proof-user-options) -(defcustom proof-three-window-enable nil +(defcustom proof-three-window-enable t "*Whether response and goals buffers have dedicated windows. If non-nil, Emacs windows displaying messages from the prover will not be switchable to display other windows. |