diff options
Diffstat (limited to 'generic/pg-response.el')
| -rw-r--r-- | generic/pg-response.el | 94 |
1 files changed, 45 insertions, 49 deletions
diff --git a/generic/pg-response.el b/generic/pg-response.el index 893d1f6f..43e0e279 100644 --- a/generic/pg-response.el +++ b/generic/pg-response.el @@ -1,12 +1,19 @@ -;; pg-response.el --- Proof General response buffer mode. -;; -;; Copyright (C) 1994-2010 LFCS Edinburgh. +;;; pg-response.el --- Proof General response buffer mode. + +;; This file is part of Proof General. + +;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh +;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: David Aspinall, Healfdene Goguen, ;; Thomas Kleymann and Dilip Sequeira + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; pg-response.el,v 12.10 2012/09/25 09:44:18 pier Exp -;; + ;;; Commentary: ;; ;; This mode is used for the response buffer proper, and @@ -85,8 +92,7 @@ ;; (defvar pg-response-special-display-regexp nil - "Regexp for `special-display-regexps' (now display-buffer-alist) -for multiple frame use. + "Regexp for ‘display-buffer-alist’ for multiple frame use. Internal variable, setting this will have no effect!") (defconst proof-multiframe-parameters @@ -99,33 +105,21 @@ Internal variable, setting this will have no effect!") "List of GNU Emacs frame parameters for secondary frames.") (defun proof-multiple-frames-enable () - ; special-display-regexps is obsolete, let us let it for a while and - ; remove it later - (unless (eval-when-compile (boundp 'display-buffer-alist)) - (let ((spdres (cons - pg-response-special-display-regexp - proof-multiframe-parameters))) - (if proof-multiple-frames-enable - (add-to-list 'special-display-regexps spdres) - (setq special-display-regexps - (delete spdres special-display-regexps))))) - ; This is the current way to do it - (when (eval-when-compile (boundp 'display-buffer-alist)) - (let - ((display-buffer-entry - (cons pg-response-special-display-regexp - `((display-buffer-reuse-window display-buffer-pop-up-frame) . - ((reusable-frames . t) - (pop-up-frame-parameters - . - ,proof-multiframe-parameters)))))) - (if proof-multiple-frames-enable - (add-to-list - 'display-buffer-alist - display-buffer-entry) - ;(add-to-list 'display-buffer-alist (proof-buffer-dislay)) - (setq display-buffer-alist - (delete display-buffer-entry display-buffer-alist))))) + (let + ((display-buffer-entry + (cons pg-response-special-display-regexp + `((display-buffer-reuse-window display-buffer-pop-up-frame) . + ((reusable-frames . t) + (pop-up-frame-parameters + . + ,proof-multiframe-parameters)))))) + (if proof-multiple-frames-enable + (add-to-list + 'display-buffer-alist + display-buffer-entry) + ;(add-to-list 'display-buffer-alist (proof-buffer-dislay)) + (setq display-buffer-alist + (delete display-buffer-entry display-buffer-alist)))) (proof-layout-windows)) (defun proof-three-window-enable () @@ -134,8 +128,10 @@ Internal variable, setting this will have no effect!") (defun proof-guess-3win-display-policy (&optional policy) "Return the 3 windows mode layout policy from user choice POLICY. -If POLIY is smart then guess the good policy from the current -frame geometry, otherwise follow POLICY." +If POLICY is ’smart then guess the good policy from the current +frame geometry, otherwise follow POLICY. + +See ‘proof-layout-windows’ for more details about POLICY." (if (eq policy 'smart) (cond ((>= (frame-width) (* 1.5 split-width-threshold)) 'horizontal) @@ -144,9 +140,10 @@ frame geometry, otherwise follow POLICY." policy)) (defun proof-select-three-b (b1 b2 b3 &optional policy) - "Put the given three buffers into three windows. -Following POLICY, which can be one of 'smart, 'horizontal, -'vertical or 'hybrid." + "Put the three buffers B1, B2, and B3 into three windows. +Following POLICY, which can be 'smart, 'horizontal, 'vertical, or 'hybrid. + +See ‘proof-layout-windows’ for more details about POLICY." (interactive "bBuffer1:\nbBuffer2:\nbBuffer3:") (delete-other-windows) (switch-to-buffer b1) @@ -186,7 +183,8 @@ Following POLICY, which can be one of 'smart, 'horizontal, (defun proof-display-three-b (&optional policy) - "Layout three buffers in a single frame. Only do this if buffers exist." + "Layout three buffers in a single frame. Only do this if buffers exist. +In this case, call ‘proof-select-three-b’ with argument POLICY." (interactive) (when (and (buffer-live-p proof-goals-buffer) (buffer-live-p proof-response-buffer)) @@ -225,9 +223,9 @@ For multiple frame mode, this function obeys the setting of For single frame mode: - In two panes mode, this uses a canonical layout made by splitting -Emacs windows in equal proportions. The splitting is vertical if -emacs width is smaller than `split-width-threshold' and -horizontal otherwise. You can then adjust the proportions by +Emacs windows in equal proportions. The splitting is vertical if +Emacs width is smaller than `split-width-threshold' and +horizontal otherwise. You can then adjust the proportions by dragging the separating bars. - In three pane mode, there are three display modes, depending @@ -243,7 +241,7 @@ dragging the separating bars. response). By default, the display mode is automatically chosen by - considering the current emacs frame width: if it is smaller + considering the current Emacs frame width: if it is smaller than `split-width-threshold' then vertical mode is chosen, otherwise if it is smaller than 1.5 * `split-width-threshold' then hybrid mode is chosen, finally if the frame is larger than @@ -254,7 +252,7 @@ dragging the separating bars. If you want to force one of the layouts, you can set variable `proof-three-window-mode-policy' to 'vertical, 'horizontal or - 'hybrid. The default value is 'smart which sets the automatic + 'hybrid. The default value is 'smart which sets the automatic behaviour described above." (interactive) (cond @@ -521,9 +519,7 @@ and start at the first error." ;; Pop up a window. (display-buffer proof-response-buffer - (and (eval-when-compile - (boundp 'display-buffer-alist)) - proof-multiple-frames-enable + (and proof-multiple-frames-enable (cons nil proof-multiframe-parameters)))))) ;; Make sure the response buffer stays where it is, ;; and make sure source buffer is visible |