search

derekelkins / agda-vim

Agda interaction in vim
BSD 2-Clause "Simplified" License
130 stars 47 forks source link

Add support for "Go to definition of identifier under point" #41

Open srghma opened 5 years ago

srghma commented 5 years ago

It s middle mouse button click or m-. in emacs mode

https://agda.readthedocs.io/en/v2.5.2/tools/emacs-mode.html

derekelkins commented 5 years ago

I've made some code to parse the annotation information that Agda provides, but it (reasonably) gives positions in terms of Unicode character offsets. This is awkward to work with with vim's byte offsets.

derekelkins commented 5 years ago

I did some shenanigans, and it should work now with <LocalLeader>d (e.g. \d) going to the definition. I haven't tested it going across files. If it doesn't seem to be working within a file, try reloading (i.e. <LocalLeader>l). Tell me if you run into any other issues with it.

srghma commented 5 years ago

tnx, seen your commit https://github.com/derekelkins/agda-vim/commit/06efbd079a7dfc0a8b079aed4509e17113cc0977#diff-41d7a2e73a1059616a22878732ea864aR426

will check

srghma commented 5 years ago

2019-01-31-22 48 27-screenshot

it's not working for me, annotations is empty

with 

    with open('/tmp/agdalog','w') as f:
        text = json.dumps(annotations)
        f.write(text)

https://asciinema.org/a/SsmzxzfYrPratGt0KruhWklYR

To reproduce

  1. clone https://github.com/srghma/programmin-language-foundations-agda-notes
  2. nix-shell (I'm using nixos)
  3. nvim