Calling Coq from within insert mode is slow

[tchajed]

There's a performance problem with triggering any prover interaction (most obviously next/previous/go to) from within insert mode. It manifests itself with these operations being much slower in insert mode than in normal mode. This is arguably a performance bug in evil (see issue #696 for the details), where the cursor color is changed too frequently when Proof General makes a bunch of set-window calls to check window properties and re-layout.

I run into this particularly often since I use F2/F3/F4 in insert mode to navigate the proof (see the customized branch of my fork), though anybody using Proof General's C-c C-n/C-c C-u/C-c C-RET bindings in insert mode will run into the same issue. I have a workaround there where I just make the insert and normal mode colors the same.

[olivierverdier]

very nice! perhaps a candidate for a pull request?