diff options
author | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2016-03-21 16:01:41 +0100 |
---|---|---|
committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2016-03-21 16:01:41 +0100 |
commit | 519a7286e3833447c8c61fd3f28b03f3e8077e4c (patch) | |
tree | 4f636f14cdaa93a1377b71987758b1a0b2eaf87c /coq/coq.el | |
parent | a27fb8390fcbdde7e1aacd61c5cc523c00386979 (diff) |
Option to toggle optimising response windo heigth.
Diffstat (limited to 'coq/coq.el')
-rw-r--r-- | coq/coq.el | 14 |
1 files changed, 12 insertions, 2 deletions
@@ -81,6 +81,11 @@ These are appended at the end of `coq-shell-init-cmd'." :type '(repeat (cons (string :tag "command"))) :group 'coq) +(defcustom coq-optimise-resp-windows-enable t + "If non-nil (default) resize vertically response windw after each command." + :type 'boolean + :group 'coq) + ;; Default coq is only Private_ and _subproof (defcustom coq-search-blacklist-string ; add this? \"_ind\" \"_rect\" \"_rec\" "\"Private_\" \"_subproof\"" @@ -1209,6 +1214,7 @@ width is synchronized by coq (?!)." :group 'coq :eval (coq-set-auto-adapt-printing-width)) + ;; defpacustom fails to call :eval during inititialization, see trac #456 (coq-set-auto-adapt-printing-width) @@ -2531,14 +2537,18 @@ Only when three-buffer-mode is enabled." (goto-char (point-min)) (recenter)))))))))) +;; TODO: remove/add hook instead? +(defun coq-optimise-resp-windows-if-option () + (when coq-optimise-resp-windows-enable (coq-optimise-resp-windows))) + ;; 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, ;; i.e. added in hook AFTER it. ;; Adapt when displaying a normal message -(add-hook 'proof-shell-handle-delayed-output-hook 'coq-optimise-resp-windows) +(add-hook 'proof-shell-handle-delayed-output-hook 'coq-optimise-resp-windows-if-option) ;; Adapt when displaying an error or interrupt -(add-hook 'proof-shell-handle-error-or-interrupt-hook 'coq-optimise-resp-windows) +(add-hook 'proof-shell-handle-error-or-interrupt-hook 'coq-optimise-resp-windows-if-option) ;;; DOUBLE HIT ELECTRIC TERMINATOR ;; Trying to have double hit on colon behave like electric terminator. The "." |