diff options
| -rw-r--r-- | CHANGES | 44 | ||||
| -rw-r--r-- | generic/pg-response.el | 5 | ||||
| -rw-r--r-- | generic/proof-useropts.el | 7 |
3 files changed, 39 insertions, 17 deletions
@@ -29,18 +29,38 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. ** Coq changes *** Smarter three windows mode: - When the frame is not large enough, the three windows are - displayed vertically, otherwise goals and response buffers are - displayed on the right. C-c C-l to refresh after resizing the - frame. - - If you want to always have goals and response buffers displayed on - the right: - (setq proof-three-window-mode-policy 'horizontal). - Always three buffers diaplayed vertically: - (setq proof-three-window-mode-policy 'vertical). - - Or via customization menus. + In three pane mode, there are three display modes, depending + where the three useful buffers are displayed: scripting + buffer, goals buffer and response buffer. + + Here are the three modes: + + - vertical: the 3 buffers are displayed in one column. + - hybrid: 2 columns mode, left column displays scripting buffer + and right column displays the 2 others. + - horizontal: 3 columns mode, one for each buffer (script, goals, + response). + + By default, the display mode is automatically chosen by + 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 + 1.5 * `split-width-threshold' then the horizontal mode is chosen. + + You can change the value of `split-width-threshold' at your + will (by default it is 160). + + 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 + behaviour described above. + + example: + + (setq proof-three-window-mode-policy 'hybrid). + + Or via customization menus. *** Multiple file handling for Coq Feature. No more experimental. Set coq-load-path to the list of directories diff --git a/generic/pg-response.el b/generic/pg-response.el index e5ecfb47..970c09ec 100644 --- a/generic/pg-response.el +++ b/generic/pg-response.el @@ -143,8 +143,9 @@ Following POLICY, which can be one of 'smart, 'horizontal, (other-window 1) (switch-to-buffer b3)) ((eq pol 'horizontal) - (display-buffer b2) ; horizontally, should be large enough + (split-window-horizontally) ; horizontally again (other-window 1) + (switch-to-buffer b2) (enlarge-window (/ (frame-width) 6) t) ; take 2/3 of width before splitting again (split-window-horizontally) ; horizontally again (other-window 1) @@ -197,7 +198,7 @@ dragging the separating bars. - horizontal: 3 columns mode, one for each buffer (script, goals, response). - By default, the display mode is automatically chosen + By default, the display mode is automatically chosen by 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' diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el index d023a67e..664ee640 100644 --- a/generic/proof-useropts.el +++ b/generic/proof-useropts.el @@ -189,9 +189,10 @@ and displayed lazily. See `proof-layout-windows'." See `proof-layout-windows'." :type '(choice - (const :tag "Horizontally if frame wide enough" smart) - (const :tag "Horizontally" horizontal) - (const :tag "Vertically" vertical)) + (const :tag "Adapt to current frame width" smart) + (const :tag "Horizontal (three columns)" horizontal) + (const :tag "Horizontal (two columns)" hybrid) + (const :tag "Vertical" vertical)) :group 'proof-user-options) |