You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Hi. I started working on Vim8/Idris2 modification that interacts through --ide-mode. I've gotten things working badly, but there are few odd things about the function of the IDE mode that I don't figure out.
What am I supposed to do when I reload a file through idris-mode? Sometimes it's giving me 'return' response and other times it's not doing that. The IDE protocol documentation doesn't tell me what kind of choreography should the editor carry out.
The another question is with the "make-case". It's giving me a nice "fill-this-in" structure. How do I properly do the replacement though?
Also interested what do you think of the code. It's asyncronously running and I tie it up together with guard functions that retry on a task when progress is made.
The text was updated successfully, but these errors were encountered:
Hi. I started working on Vim8/Idris2 modification that interacts through
--ide-mode
. I've gotten things working badly, but there are few odd things about the function of the IDE mode that I don't figure out.https://github.com/cheery/idris-vim
https://github.com/cheery/idris-vim/blob/master/ftplugin/idris.vim
What am I supposed to do when I reload a file through idris-mode? Sometimes it's giving me 'return' response and other times it's not doing that. The IDE protocol documentation doesn't tell me what kind of choreography should the editor carry out.
The another question is with the "make-case". It's giving me a nice "fill-this-in" structure. How do I properly do the replacement though?
Also interested what do you think of the code. It's asyncronously running and I tie it up together with guard functions that retry on a task when progress is made.
The text was updated successfully, but these errors were encountered: