diff options
| -rw-r--r-- | coq/coq.el | 82 | ||||
| -rw-r--r-- | generic/proof-shell.el | 8 |
2 files changed, 53 insertions, 37 deletions
@@ -2627,19 +2627,24 @@ buffer." First goal is displayed on the bottom of its window, maximizing the number of hypothesis displayed, without hiding the goal" (interactive) - (let ((pg-frame (car (coq-find-threeb-frames)))) ; selecting the good frame - (with-selected-frame (or pg-frame (window-frame (selected-window))) - ;; prefer current frame - (let ((goal-win (or (get-buffer-window proof-goals-buffer) (get-buffer-window proof-goals-buffer t)))) - (if goal-win - (with-selected-window goal-win - ;; find snd goal or buffer end - (search-forward-regexp "subgoal 2\\|\\'") - (beginning-of-line) - ;; find something else than a space - (ignore-errors (search-backward-regexp "\\S-")) - (recenter (- 1)) ; put it at bottom og window - (beginning-of-line))))))) + ;; CPC 2015-12-31: Added the check below: if the command that caused this + ;; call was silent, we shouldn't touch the goals buffer. See GitHub issues + ;; https://github.com/cpitclaudel/company-coq/issues/32 and + ;; https://github.com/cpitclaudel/company-coq/issues/8. + (unless (memq 'no-goals-display proof-shell-delayed-output-flags) + (let ((pg-frame (car (coq-find-threeb-frames)))) ; selecting the good frame + (with-selected-frame (or pg-frame (window-frame (selected-window))) + ;; prefer current frame + (let ((goal-win (or (get-buffer-window proof-goals-buffer) (get-buffer-window proof-goals-buffer t)))) + (if goal-win + (with-selected-window goal-win + ;; find snd goal or buffer end + (search-forward-regexp "subgoal 2\\|\\'") + (beginning-of-line) + ;; find something else than a space + (ignore-errors (search-backward-regexp "\\S-")) + (recenter (- 1)) ; put it at bottom og window + (beginning-of-line)))))))) (defvar coq-modeline-string2 ")") (defvar coq-modeline-string1 ")") @@ -2704,30 +2709,33 @@ number of hypothesis displayed, without hiding the goal" (defun coq-optimise-resp-windows () "Resize response buffer to optimal size. Only when three-buffer-mode is enabled." - ;; If there is no frame with goql+response then do nothing - (when (and proof-three-window-enable (coq-find-threeb-frames)) - (let ((pg-frame (car (coq-find-threeb-frames)))) ; selecting one adequat frame - (with-selected-frame pg-frame - (when (and (> (frame-height) 10) - (get-buffer-window proof-response-buffer)) - (let ((maxhgth - (- (+ (with-selected-window (get-buffer-window proof-goals-buffer t) (window-text-height)) - (with-selected-window (get-buffer-window proof-response-buffer t) (window-text-height))) - window-min-height)) - hgt-resp nline-resp) - (with-selected-window (get-buffer-window proof-response-buffer) - (setq hgt-resp (window-text-height)) - (with-current-buffer proof-response-buffer - (setq nline-resp ; number of lines we want for response buffer - (min maxhgth (max window-min-height ; + 1 for comfort - (+ 1 (count-lines (point-max) (point-min))))))) - (unless (is-not-split-vertic (selected-window)) - (shrink-window (- hgt-resp nline-resp))) - (with-current-buffer proof-response-buffer - (goto-char (point-min)) - (recenter))))))))) - - + ;; CPC 2015-12-31: Added the check below: if the command that caused this + ;; call was silent, we shouldn't touch the response buffer. See GitHub + ;; issues https://github.com/cpitclaudel/company-coq/issues/32 and + ;; https://github.com/cpitclaudel/company-coq/issues/8. + (unless (memq 'no-response-display proof-shell-delayed-output-flags) + ;; If there is no frame with goql+response then do nothing + (when (and proof-three-window-enable (coq-find-threeb-frames)) + (let ((pg-frame (car (coq-find-threeb-frames)))) ; selecting one adequat frame + (with-selected-frame pg-frame + (when (and (> (frame-height) 10) + (get-buffer-window proof-response-buffer)) + (let ((maxhgth + (- (+ (with-selected-window (get-buffer-window proof-goals-buffer t) (window-text-height)) + (with-selected-window (get-buffer-window proof-response-buffer t) (window-text-height))) + window-min-height)) + hgt-resp nline-resp) + (with-selected-window (get-buffer-window proof-response-buffer) + (setq hgt-resp (window-text-height)) + (with-current-buffer proof-response-buffer + (setq nline-resp ; number of lines we want for response buffer + (min maxhgth (max window-min-height ; + 1 for comfort + (+ 1 (count-lines (point-max) (point-min))))))) + (unless (is-not-split-vertic (selected-window)) + (shrink-window (- hgt-resp nline-resp))) + (with-current-buffer proof-response-buffer + (goto-char (point-min)) + (recenter)))))))))) ;; TODO: I would rather have a response-insert-hook thant this two hooks ;; Careful: coq-optimise-resp-windows must be called BEFORE proof-show-first-goal, diff --git a/generic/proof-shell.el b/generic/proof-shell.el index cb9ed2bb..4f89963e 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1658,6 +1658,14 @@ i.e., 'goals or 'response." ;; indicate that (only) a response output has been given 'response)) + ;; FIXME (CPC 2015-12-31): The documentation of this hook suggests that it + ;; only gets run after new output has been displayed, but this isn't true at + ;; the moment: indeed, it gets run even for invisible commands. + ;; + ;; This causes issues in company-coq, where completion uses invisible + ;; commands to display the types of completion candidates; this causes the + ;; goals and response buffers to scroll. I fixed it by adding checks to + ;; coq-mode's hooks, but maybe we should do more. (run-hooks 'proof-shell-handle-delayed-output-hook))) |