diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2007-04-20 12:24:52 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2007-04-20 12:24:52 +0000 |
| commit | 132c172e4012eabb1089694e86ecf2f6507c7444 (patch) | |
| tree | ae39231ef777a60d66a4013b93736c4b56d2b91f /coq | |
| parent | 90231d87be16f95f5930b14d2a214e0d8bb6eb86 (diff) | |
Add a shrink adapting hook for coq response buffer.
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq.el | 10 | ||||
| -rw-r--r-- | coq/x-symbol-coq.el | 2 |
2 files changed, 8 insertions, 4 deletions
@@ -144,10 +144,10 @@ controling coq prompt. Only for coq >= 8.1 (and 8.1 beta)") ;; (concat "(\\*\\|" (concat "[ ]*" (regexp-opt '( - "Ltac" "Corr" "Modu" "Sect" "Chap" "Goal" "Definition" "Lemm" "Theo" "Fact" "Rema" "Mutu" "Fixp") t))) + "Ltac" "Corr" "Modu" "Sect" "Chap" "Goal" "Definition" "Lemm" "Theo" "Fact" "Rema" "Mutu" "Fixp" "Func") t))) ;) -(defvar coq-outline-heading-end-regexp "\\*\)\n\\|\\.[ \t\n]\\|:=") +(defvar coq-outline-heading-end-regexp "\\.[ \t\n]") (defvar coq-shell-outline-regexp coq-goal-regexp) (defvar coq-shell-outline-heading-end-regexp coq-goal-regexp) @@ -1545,12 +1545,16 @@ buffer." (setq hgt-resp (window-height)) (setq nline-resp (min maxhgth (max 5 (count-lines (point-max) (point-min))))) - (shrink-window (- hgt-resp nline-resp)) + (shrink-window (- hgt-resp (+ 1 nline-resp))) (beginning-of-buffer) (recenter) (select-window curwin)))) +;; TODO: I would rather have a response-insert-hook thant this two hooks +;; Adapt when displaying a normal message (add-hook 'proof-shell-handle-delayed-output-hook 'optim-resp-windows) +;; Adapt when displaying an error or interrupt +(add-hook 'proof-shell-handle-error-or-interrupt-hook 'optim-resp-windows) diff --git a/coq/x-symbol-coq.el b/coq/x-symbol-coq.el index 98c53c09..3a286db6 100644 --- a/coq/x-symbol-coq.el +++ b/coq/x-symbol-coq.el @@ -96,7 +96,7 @@ See `x-symbol-header-groups-alist'." ;;;=========================================================================== (defcustom x-symbol-coq-subscript-matcher 'x-symbol-coq-subscript-matcher - "Function matching super-/subscripts for language `isa'. + "Function matching super-/subscripts for language `coq'. See language access `x-symbol-LANG-subscript-matcher'." :group 'x-symbol-coq :type 'function) |