Goto Definition is off by one

[m0rphism]

Consider the following code:

open import Data.Nat
                -- cursor jumps to this line
x : ℕ           -- cursor should jump to this line
x = {! !}

y = x           -- cursor is on this x when running GotoDefinition

If using CornelisGotoDefinition on the x in the definition of y, then the cursor jumps not to the line with x : ℕ, but to the empty line above it. This seems to happen independently of what code is around the definition and how far the uses and definitions are apart from each other.

Thanks for the great plugin! <3

I'm currently switching from emacs to nvim, and apart from #153 and #121 this plugin seems to have everything I need. Keep up the great work! :)

[isovector]

Weird. This is definitely a regression, but I can indeed reproduce it :confused:

I'm not actively writing any Agda these days, so it might take some time to tackle this one.

[isovector]

This is almost certainly the problem:

https://github.com/isovector/cornelis/blob/06d6020eed1a3520bb2887337dd5b27b1755968b/src/Plugin.hs#L68

which a quick fix might be

      let buffer_idx = toBytes contents $ incIndex $ zeroIndex $ ds_position ds

The vim API has at least four different indexing modes, and it's hard to make sure we pick the right one in each case :(

[m0rphism]

Nice! I just tested it in a fork, and it indeed fixes the bug. :+1:

Thanks for the quick help! :clap:

The vim API has at least four different indexing modes, and it's hard to make sure we pick the right one in each case :(

Yeah, I can imagine... I yet have to find a text editor API, which doesn't make me want to pull my hair out ;)