diff options
| -rw-r--r-- | coq/coq.el | 55 | ||||
| -rw-r--r-- | generic/pg-response.el | 22 |
2 files changed, 60 insertions, 17 deletions
@@ -1187,21 +1187,60 @@ necessary.") (defun coq-reset-printing-width () (setq coq-shell-current-line-width nil)) -(defun coq-goals-window-width () +(defun coq-buffer-window-width (buffer) + "Return the width of a window currently displaying BUFFER." (let* - ((goals-wins (get-buffer-window-list proof-goals-buffer nil t)) - (dummy (if (not (eq 1 (length goals-wins))) - (message "Zero or more than one goals window, guessing window width."))) - (goal-win (car goals-wins))) - (window-width goal-win))) + ((buf-wins (get-buffer-window-list buffer nil t)) + (dummy (if (not (eq 1 (length buf-wins))) + (display-warning + 'proof-general + "Zero or more than one goals window, guessing window width." + :debug))) + (buf-win (car buf-wins)));; TODO return the widest one instead of the first? + ;; return nil if no goal buffer found + (and buf-win (window-width buf-win)))) + + +(defun coq-goals-window-width () + (coq-buffer-window-width proof-goals-buffer)) +(defun coq-response-window-width () + (coq-buffer-window-width proof-response-buffer)) + +(defun coq-guess-goal-buffer-at-next-command () + "Return the probable width of goals buffer if it pops up now. +This is a guess based on the current width of goals buffer if +present, current pg display mode and current geometry otherwise." + (let (pol (proof-guess-3win-display-policy proof-three-window-mode-policy)) + (cond + ;; goals buffer is visible, bingo + ((coq-goals-window-width)) + ;; Below is the heuristic to guess the good width for goals + ;; 2 windows mode, response-buffer visible, use this width + ((and (not proof-three-window-enable) (coq-response-window-width))) + ;; 2 windows mode, response buffer not visible, give up + ((not proof-three-window-enable) nil) + ;; 3 windows mode, one frame, and vertical policy + ((and proof-three-window-enable (not proof-multiple-frames-enable) + (eq pol 'vertical)) + (window-width)) + ;; 3 windows mode, one frame, other policies, give up + ((and proof-three-window-enable (not proof-multiple-frames-enable)) + nil) + ;; multiple frames. If goals buffer pops up it will have frame default + ;; size. Falling back to X default window size if not specified. + ;; This is hard to mimick, let us give up + (proofproof-multiple-frames-enable nil) + (t nil) ;; assert false? + ))) (defun coq-adapt-printing-width (&optional show width) "Sends a Set Printing Width command to coq to fit the response window's width. A Show command is also issued if SHOW is non-nil, so that the goal is redisplayed." (interactive) - (let ((wdth (or width (coq-goals-window-width)))) - (when (not (equal wdth coq-shell-current-line-width)) + (let ((wdth (or width (coq-guess-goal-buffer-at-next-command)))) + ;; if no available width, or unchanged, do nothing + (when (and wdth (not (equal wdth coq-shell-current-line-width))) (proof-shell-invisible-command (format "Set Printing Width %S." (- wdth 1)) t) (setq coq-shell-current-line-width wdth) ;; Show iff show non nil and some proof is under way diff --git a/generic/pg-response.el b/generic/pg-response.el index e278cec3..e903858e 100644 --- a/generic/pg-response.el +++ b/generic/pg-response.el @@ -130,6 +130,18 @@ Internal variable, setting this will have no effect!") (defun proof-three-window-enable () (proof-layout-windows)) + +(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 (eq policy 'smart) + (cond + ((>= (frame-width) (* 1.5 split-width-threshold)) 'horizontal) + ((>= (frame-width) split-width-threshold) 'hybrid) + (t 'vertical)) + 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, @@ -137,15 +149,7 @@ Following POLICY, which can be one of 'smart, 'horizontal, (interactive "bBuffer1:\nbBuffer2:\nbBuffer3:") (delete-other-windows) (switch-to-buffer b1) - (let ((pol)) - (if (eq policy 'smart) - (cond - ((>= (frame-width) (* 1.5 split-width-threshold)) - (setq pol 'horizontal)) - ((>= (frame-width) split-width-threshold) - (setq pol 'hybrid)) - (t (setq pol 'vertical))) - (setq pol policy)) + (let ((pol (proof-guess-3win-display-policy policy))) (save-selected-window (cond ((eq pol 'hybrid) |