search

cpitclaudel / company-coq

A Coq IDE build on top of Proof General's Coq mode
GNU General Public License v3.0
353 stars 29 forks source link

code completion should not interrupt search #186

Open JasonGross opened 6 years ago

JasonGross commented 6 years ago

If I do C-s Goal, then I get command completion at the first location of Goal in my code; if I keep typing, it ends up in the document, rather than in the search buffer. This is very annoying.

Command sequence: C-s Goal True: bad-search

cpitclaudel commented 6 years ago

Huh. Something's wrong with your Emacs :) Or, more likely, I need more details to reproduce this.

JasonGross commented 6 years ago

Hmmm, well, it doesn't seem to happen with a freshly opened emacs, so something really strange is going on.... (For reference, this is emacs 24.5.1)