Fixed go to definition to work with Agda 2.6+, improved unicode support, added support for python 3

[1000000000]

Go to definition

• Fixed regex for parsing annotations to match up with the formatting described in the link above parseAnnotation
• Changed highlighting level for load commands sent to Agda process to "Interactive" so that Agda 2.6+ will provide annotation information.

Improved unicode support, added support for python 3

• Used vimscript more heavily to get better consistency with handling unicode characters fixing errors finding goals when unicode characters appear in the line before the goal
• Switched to unicode strings by default ala python 3 to fix encode/decode errors that occurred when operating on goal bodies that contained unicode characters
• Fixed use of field names only present in python 2 and not 3 and modified the function exposer to call the vim python command associated with the version of python running the script
• Changed the behavior of the vim script to use python 3 if possible and use python 2 as a fallback.

[derekelkins]

Testing with Python 3.8.3, vim 8.2, and Agda 2.6.1, this did not initially work. The issue was the handling of the include paths. Changing vim.vars['agdavim_agda_includepathlist'] to map(lambda bs: str(bs, 'utf-8'), vim.vars['agdavim_agda_includepathlist']) in the two relevant locations in sendCommandLoad resolved the issue.

However, there are still issues. Using this example:

data ℕ : Set where
    z : ℕ
    s : ℕ → ℕ

foo : ℕ → ℕ
foo = λ { x → ? }

if you perform a case analysis on x it produces:

foo = λ { z → {!   !}; (s x) → {!   !}

which is missing the final "}", breaking the code.

[1000000000]

Thanks for the response, I'll check it out

[canndrew]

Would it be possible to just merge the "added python 3 support" commit from this PR if it's the other commit which is causing problems? NixOS recently removed python 2 support from their neovim, so I was stuck with no agda support in neovim until I discovered that I can just cherry-pick that commit to get it back (thanks @1000000000 😁)

[VictorTaelin]

Did the changes recommended above, on https://github.com/victortaelin/agda-vim in case anyone needs it