derekelkins / agda-vim

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

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

Open 1000000000 opened 4 years ago

1000000000 commented 4 years ago

Go to definition

Improved unicode support, added support for python 3

derekelkins commented 4 years ago

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 commented 4 years ago

Thanks for the response, I'll check it out

canndrew commented 3 years ago

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 :grin:)

VictorTaelin commented 1 year ago

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