idris-mode icon indicating copy to clipboard operation
idris-mode copied to clipboard

integrate idris-mode and idris2-mode

Open ywata opened this issue 3 years ago • 0 comments

As I tried idris-mode and idris2-mode, I did not understand the difference. So, I changed idris2- etc into idris-, and manual modification to minimize the difference. I found, there are not so much difference between the two. If it is possible, I'd like to propose to merge back to idris2-mode into idris-mode to reduce maintenance efforts.

Actually, I'm not fully understand the detail but I analyzed the difference. The updated branches are in my repository. https://github.com/ywata/idris-mode idris-mode-working and idris2-mode-working diff.txt

I marked DECISION N to indicate items we need to decide and NEED INVESTIGATION to mark which I'm not sure about at this moment. The diffs are from my repository https://github.com/ywata/idris-mode diff between idris-mode-working and idris2-mode-working. They are normalized to make diff minimal.

Could you take a look at the diff?

ywata avatar Jul 28 '21 11:07 ywata