search

cpitclaudel / company-coq

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

It should be easy to [discover how to] disable code folding #204

Open JasonGross opened 6 years ago

JasonGross commented 6 years ago

Code folding is by far the most annoying feature of company-coq for me; I use TAB in the middle of a line to indent my code, and sometimes I hit TAB just before lifting my finger off of SHIFT when typing something like { TAB reflexivity. Normally, this would just cause the line to be not indented, but with company-coq, this causes my reflexivity to go in the wrong place, and I have to backtrack to the location of the open brace to unfold my code, and then move my cursor back to where I was typing. This easily happens multiple times an hour. (The first couple of times it happened, I had to close the file and re-open it, because I couldn't figured out what had happened or how to get my code back.)

How do I disable this feature?

cpitclaudel commented 6 years ago

How do I disable this feature?

The usual way: M-x customize-group RET company-coq RET, then expand "Company Coq Disabled Features", and check "Code folding"

JasonGross commented 6 years ago

Thanks! Is there a way to disable it from my ~/.emacs (so that when I copy the config to a new machine, I get this automatically)?

cpitclaudel commented 6 years ago

The process I just described should do that, yes (click "save for future sessions")

cpitclaudel commented 5 years ago

Thinking more about this, the right approach might be to show a small message when code is folded using S-TAB; how does that sound? The message would explain how to unfold.