Open TimRichter opened 9 years ago
I have the same problem. To work around it, try :set filetype=idris
when you're editing a .lidr file. It looks like idris-vim isn't recognising the filetype.
Hmmm, there is support: https://github.com/idris-hackers/idris-vim/blob/master/ftdetect/lidris.vim
That sets filetype to "lidris" not "idris". Seems that the repl depends on "idris".
When I try :set filetype=idris
I can evaluate the buffer once, but when I do it a second time I get the following error popping up in the REPL:
Idris> Symbol "idris_mkFileError" not found
idris: user error (Could not call foreign function "idris_mkFileError" with args [prim__vm (prim__TheWorld)])
I guess that simply forcing vim to see literate files as regular ones gets it confused somehow, perhaps because the .ibc
file isn't properly created.
I'm not sure whether this is an issue with idris-vim or just with my setup, please bear with me.
When editing .lidr (literate idris) files, and doing the key combinations that should call the REPL, i.e. r , nothing happens. What am I doing wrong?