search

ashinkarov / nvim-agda

Agda interaction pluging for neovim
36 stars 5 forks source link

Develop #7

Open shinji-kono opened 2 years ago

shinji-kono commented 2 years ago

JumpToError counslt error message contents (byte2line won't work because of neovim's unapplied patch) add indent on make case handling chose different syntax on hole and unsolved metas ingnore error on normalize

ashinkarov commented 2 years ago

@shinji-kono , I wrote a bunch of comments (in-line with your original changes). I am just wondering if you have seen these? There are even more new features added recently, but none of the concerns are yet addressed. I guess it would be easier if we could keep use one pull request per one logical change.

shinji-kono commented 2 years ago

Ya, that's make sense. I think I checked your update, but I missed some.