search

idris-hackers / idris-mode

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

Idris2: display one line error message in minibuffer #563

Closed keram closed 1 year ago

keram commented 1 year ago

Change in IDE protocol in causes same error message being displayed in Emacs minibuffer and also in idris-notes buffer.

Interestingly Idris/REPL.idr https://github.com/idris-lang/Idris2/blob/main/src/Idris/REPL.idr#L1241-L1242` prints out only filename as expected, while IDEMode/REPL.idr https://github.com/idris-lang/Idris2/blob/main/src/Idris/IDEMode/REPL.idr#L362-L363 prints also whole error causing this issue.

Maybe we will be able to change the behaviour in Idris2 so making this PR for time being as a draft.

Before change:

async-minibuffer-before-change-idris2

After change:

async-minibuffer-after-change-idris2

Idris 1.3 before/after change:

async-minibuffer-after-and-before-change-idris1-3

keram commented 1 year ago

May be fixed in https://github.com/idris-lang/Idris2/pull/2768

jfdm commented 1 year ago

Even if the issue has been addressed in Idris2, the issue will remain for Idris1. Perhaps, but maybe not, we should address it for Idris1.

But this can be a low priority issue, as Idris2 is developed more than Idris1.

keram commented 1 year ago

Even if the issue has been addressed in Idris2, the issue will remain for Idris1. Perhaps, but maybe not, we should address it for Idris1.

The Idris1 does not have the same issue, please see the last screenshot in description :) Btw what would be the best way to discuss generic maintainance of the idris-mode, (discord, email, irc)?

keram commented 1 year ago

Closing as the fix was merged directly to Idris2 and does mean we don't have to do any changes.

jfdm commented 1 year ago

Btw what would be the best way to discuss generic maintainance of the idris-mode, (discord, email, irc)?

Erm, if you message me (privately or perhaps better in the open on a relevant thread) on the Idris discord I will try to respond promptly. I say try as: Discord notifications are borked for me in that I do not receive them at all---related to mobile client settings and app settings interfering with each other.

Thanks for the work you are putting into the mode.

keram commented 1 year ago

Btw what would be the best way to discuss generic maintainance of the idris-mode, (discord, email, irc)?

I say try as: Discord notifications are borked for me in that I do not receive them at all---related to mobile client settings and app settings interfering with each other.

@jfdm https://discord.com/channels/827106007712661524/1045022104577396847