search

idris-hackers / idris-mode

Idris syntax highlighting, compiler-supported editing, interactive REPL and more things for Emacs.
GNU General Public License v3.0
268 stars 70 forks source link

Case splitting results in non-unique hole name #512

Closed scotek closed 3 years ago

scotek commented 4 years ago

Continuing from idris-lang/Idris2#566 , case-splitting can omit the last character resulting in non-unique hole names.

Removing the 1- call in the handling on idris-case-split in gets the full output to appear for me (https://github.com/idris-hackers/idris-mode/blob/b77eadd8ac2048d5c882b4464bd9673e45dd6a59/idris-commands.el#L582). The root cause seems to go back to #466 .

The problem appears to affect idris-make-cases-from-hole as well, with the same fix. I'll look at a couple of other possible places then do a PR.

scotek commented 4 years ago

The issue seems to be limited to idris-case-split and idris-make-cases-from-hole.

Removing (1- from both works well for Idris 2, but results in an extra newline being inserted in Idris 1 (1.3.2-git:476234f8a). It still produces a valid substitution but does mean the user will have to backspace the extra newline after the keystoke. There doesn't seem to be an easy way to identify which version of Idris is being used - I don't think the protocol version was changed.

jfdm commented 4 years ago

@scotek Thanks for the contribution, I think what we are seeing are differences slowly appearing in the ide-protocol. So we either ensure that the ide-protocol implementations are kept the same or we need to diverge... TBH your observation in #513 is rather prudent:

We may need to look at adding a setting to indicate Idris 1 vs 2 and tweak some of these functions but that needs a separate discussion.

IIRC the ide-protocol does allow one to get the Idris version from the compiler, maybe we need to check/extend the ide-protocol with protocol versioning to allow a mode to be backwards and forward compatible. I am happy to mentor this, and it is something we should raise on the mailing list for action.

jfdm commented 3 years ago

fixed in #513 and #519