Closed trillioneyes closed 3 years ago
Ach! This was my mistake on merging some upstream functionality taken from the idris-community/idris2-mode repository.
For context, idris-mode was designed as the emacs-mode that interacts with a compiler using the idris-ide-protocol. Technically, idris-mode should be able to interoperate with any compiler that supports the idris-ide-protocol. Idris1 supports version 1 of the protocol, and Idris2 supports version 2. Over the last year, some people decided to develop an Idris2-mode that only supports version 2 of the ide-protocol. Idris-mode is still ticking because there are a few people that still use idris1, and some of us want to see an Idris-mode that supports all versions of the protocol.
There is some recent happenings that will see the two respective emacs-modes (idris-mode and idris2-mode) resolve there differences. In the mean time, both modes should work, but there might be a disparity about how much of the protocol version 2 that they each support.
I am merging this because I did a bad PR myself. I will revisit the functionality that I should have added at a later date.
i just started to learn idris2 using the book, and idris-mode in emacs. and i have just met this bug.
could this be merged please?
also, what is idris2-mode? am i using the wrong emacs mode in my context?