Displaying the completion list should not reset position in the *goals* buffer

[JasonGross]

When I have a large goal, and I am scrolled to a particular point in the *goals* buffer, if I type something, and the completion drop-down shows up, the *goals* buffer resets to its default scroll point, much the same way that it does when I execute Show. or C-c C-p. This is annoying, as it means I can't refer to a particular point in the goal while typing things.

[JasonGross]

This seems to be tied to displaying types in the minibuffer; it shows up for completing theorems (which displays their type in the minibuffer), but not for completing, e.g., Add Parametric Relation.

[cpitclaudel]

I think your analysis is right. The problem is probably due to coq-PG reprinting the goal when a new command is issued. I may be able to do something on the company-coq side, but it's really a PG issue.

[cpitclaudel]

Could you try this fix when it lands into MELPA? It should fix this bug.

[JasonGross]

Thanks! Can you ping me when it lands in MELPA?

[cpitclaudel]

Sure

[cpitclaudel]

Note to self. The fix for this should really be merged into PG; atm company-coq saves the buffer position before calling the prover, and resets the position after calling it, causing disagreeable jitter.

[cpitclaudel]

Should be in MELPA now :)

[lczch]

I have this problem too.
When I want to type something according goals or responds, the point immediately jump to buffer-begin.
It's somewhat annoying :(
Version Information:
company-coq: 20150718.1931
proof-general: latest master branch
Emacs: 24.3.1

[cpitclaudel]

Hi @lczch . Can you give me a bit more details? This problem should have been fixed a while back.
What do you mean by "When I want to type something according goals or responds"?

[cpitclaudel]

Pushed a cleaner fix to a branch of PG at https://github.com/ProofGeneral/PG/tree/fix-scrolling-buffers.