search

whonore / Coqtail

Interactive Coq Proofs in Vim
MIT License
272 stars 35 forks source link

Is redraw necessary on panel refresh? #221

Closed tomtomjhj closed 2 years ago

tomtomjhj commented 3 years ago

coqtail#panels#refresh runs :redraw at the end. https://github.com/whonore/Coqtail/blob/358747255db85579498dfc6e03dcd808d5b81d34/autoload/coqtail/panels.vim#L324 This has various side effects such as flickering cursor (Vim) and disappearing IncSearch highlights (both Vim and NeoVim), which are quite annoying. I have been using Coqtail for a few days with that line removed, and it seems to work well. So I think it makes sense to remove that line if there is no specific need for it (which I could not find from git history).

whonore commented 3 years ago

The origin of that redraw command seems to date back to the first commit, which was copied from when I forked Coquille, so it very well may not be necessary. I would imagine that the worst removing it could do is to slightly delay updating the highlighting for the checked region, but there's already a bit of delay because of how the async code works so it should be fine. Maybe keep testing it a couple more days and I will too and if everything seems fine we can remove it.

whonore commented 3 years ago

"A couple more days" ended up being longer than I anticipated, but I finally got around to trying this. I started getting occasional strange errors about there being no :endif on line 26 of s:call, which must mean something is going wrong in evalexpr. I don't understand how removing redraw could be related, but I stop seeing the errors when I put it back.

All I can think of is that it's probably some unrelated async bug that's just masked by the extra time taken by redraw. If you don't see these errors in NeoVim then that's another good argument to avoid ch_evalexpr altogether and just implement our own polling loop (see #224). But until I have time to look into this further I'm going to leave redraw.

whonore commented 3 years ago

I may have spoken too soon because I'm still seeing the error even with redraw, though much less frequently.