search

ashinkarov / nvim-agda

Agda interaction pluging for neovim
36 stars 5 forks source link

"Don't know how to handle JumpToError" #10

Closed tomsmeding closed 1 year ago

tomsmeding commented 1 year ago

I'm probably doing something wrong, but I just installed nvim-agda (using vim-plug) as well as lua-utf8 for lua 5.1, but loading (<localleader>l) a file containing an error produces the error message in the title.

Terminal session recording here: https://asciinema.org/a/0iRhEVSdTfPNj4KZEbPdwbthb

OS: Arch Linux nvim: v0.8.3

ashinkarov commented 1 year ago

The problem is that the debugging output is left on in the plugin, and it is mixed with the error message, as they are both printing in the same stream. There are few messages (such as JumpToError that agda sends out, but the plugin doesn't yet handle). Your input x indeed does not typecheck, which is relected in the error message, but also spolied by debug output. If you write something like

F : Set → Set
F X = X → X

in your test.agda it will work fine.

I have just updated the plugin to turn debugging info on, and I will turn this into the option.

ashinkarov commented 1 year ago

Please update the plugin and see whether it works as expected.

ashinkarov commented 1 year ago

Ok, it is an option now.

tomsmeding commented 1 year ago

Yep, that fixes it! Thanks for the quick fix :)

Turns out I prefer the separate-window interface of a different plugin (which unfortunately has less command coverage). I'll see what I do.

ashinkarov commented 1 year ago

@tomsmeding , what is exactly meant by separate-window here? Most of the things are in the floating window, and the rest is available throug :messges. Anyhow, the plugin is quite straight-forward to hack, it is quite simple, so feel free to send a pull request. At the end of the day, I presume it is just about figuring out where do you want to print things to, which is close to trivial to change.