aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <Pierre.Courtieu@gmail.com>2016-01-06 17:41:08 +0100
committerGravatar Pierre Courtieu <Pierre.Courtieu@gmail.com>2016-01-06 17:41:08 +0100
commita608501960ce8b00d42840f779ae7983b8363c86 (patch)
tree0511be95a36aa572ddc85760e2a6e3340ba42edb /generic
parentba1187827393aa651b2814d513749b43d0bcc772 (diff)
parente3d4762275b810307acf865c124b1265bc01a5d8 (diff)
Merge pull request #22 from ProofGeneral/fix-scrolling-buffers
Fix spurious scrolling of *goals* and *response* buffers
Diffstat (limited to 'generic')
-rw-r--r--generic/proof-shell.el8
1 files changed, 8 insertions, 0 deletions
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)))