search

whonore / Coqtail

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

Add CoqCommandComplete and g:coqtail#event #368

Open whonore opened 2 months ago

whonore commented 2 months ago

Fixes #367.

whonore commented 2 months ago

@katrinafyi could you see if the approach described in the docs here does what you want?

katrinafyi commented 2 months ago

I'll give it a try today, thanks!

katrinafyi commented 2 months ago

Thanks for working on this!

Using the autocmd in the documentation seems to hang the editor. Is there a cycle with CoqJumpToEnd triggering it again?

I tried this and it did not seem to fix the problem, but my Vimscript is not good:

let g:coqautocommanding = v:false
augroup CoqtailFollowChecked
autocmd!
autocmd! User CoqCommandComplete
\  if ! g:coqautocommanding && g:coqtail#event.cmd =~# 'step\|rewind\|to_line\|to_top'
\|   let g:coqautocommanding = v:true
\|   CoqJumpToEnd
\|   let g:coqautocommanding = v:false
\| endif
augroup END

I can confirm that the autocmd works if I replace the CoqJumpToEnd with a simple echo.

whonore commented 2 months ago

Ah, I bet it's the same root problem as #360. I was able to work around it then but I guess I'll have to figure out how to actually solve it. In the meantime, it works for me at least using Vim instead of NeoVim.