diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-12-31 17:48:47 +0100 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-12-31 17:52:38 +0100 |
| commit | e3d4762275b810307acf865c124b1265bc01a5d8 (patch) | |
| tree | 8e660e382b3481dc29ede31e9d0be3cac9ba1ab9 /generic | |
| parent | e0e2ceaa1bc1750fc05b4589351e10a1081453dd (diff) | |
Fix spurious scrolling of *goals* and *response* buffers
See https://github.com/cpitclaudel/company-coq/issues/8 and
https://github.com/cpitclaudel/company-coq/issues/32 for some background
info.
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-shell.el | 8 |
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))) |