whonore / Coqtail

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

Vim is slow to jump using G in .v files #236

Closed ana-borges closed 2 years ago

ana-borges commented 2 years ago

For example, 10G, or GG take a couple of seconds, but it's annoying when the expectation was that this would be instantaneous. It happens in .v files whether or not CoqStart has already been called, and it does not happen in files without the .v extension. It happens in short files (10 lines) and longer ones (400 lines). Let me know if I can provide some useful debugging information.

tomtomjhj commented 2 years ago

Coqtail has default mappings that start with G (G[ and G]). Since G is the prefix of those maps, vim waits for the timeout specified by Vim's timeoutlen option to decide what you meant by G (G vs G[ or G]). You can prevent this by disabling the default mappings altogether with let g:coqtail_nomap = 1 or unmapping those particular mappings in FileType coq autocmd or after/ftplugin/.

I think Coqtail shouldn't map G[ and G] by default because they are too intrusive.

ana-borges commented 2 years ago

Great, I'm relieved it has such a simple explanation!

I added this to my .vimrc:

au FileType coq unmap <buffer> G[
au FileType coq unmap <buffer> G]

but it doesn't actually disable anything. It does work from inside a session with :unmap <buffer> G[, and then G is fast again. Is this the wrong way to go about it? (Disabling every mapping works, but I'd rather not.)

whonore commented 2 years ago

Thanks for reporting. The reason that doesn't work in .vimrc is because it's sourced before the Coqtail mappings are defined. I think it should work if you put those in after/ftplugin/coq.vim. Alternatively, if you want to keep the mappings, but use ones that don't conflict and are consistent with other Vim commands you could use:

nmap <buffer> ]g <Plug>CoqGotoGoalNextStart
nmap <buffer> ]G <Plug>CoqGotoGoalNextEnd
nmap <buffer> [g <Plug>CoqGotoGoalPrevStart
nmap <buffer> [G <Plug>CoqGotoGoalPrevEnd

This will also prevent Coqtail from mapping G] and G[. This is actually what I use, which is why I didn't notice the conflict with G (oops). I'll try to fix this and the related #171 soon.

tomtomjhj commented 2 years ago

More precisely, the order of ftplugin/coq.vim and au FileType coq depends on how your vimrc is organized. If your vimrc runs filetype plugin on (call plug#end() does this) before the custom au FileTypes, ftplugin/ runs before au FileTypes. This is because filetype plugin on is implemented as au FileType. See also :h :filetype-plugin-on.