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

Make empty string always return value from `idris-process-filter` #564

Closed keram closed 1 year ago

keram commented 1 year ago

Why: In commit: https://github.com/idris-hackers/idris-mode/commit/74731b53caa6b2a2a was introduced regression by moving the "" inside of the if expression causing it being return value only in some cases. The return value from idris-process-filter is written into idris-process buffer and after commit 74731b53caa6b2a2a this become mostly the output of idris-connect which consequently returns idris-words-of-encouragement. Because now the *idris-process* buffer is not empty it is moved to the front and interrupts users workflow.

Downside of this fix is that the words of encouragement may be lost from users sight due to another messages when loading file to Idris. This will be addressed in separate commit.

Before fix:

https://user-images.githubusercontent.com/578608/201521721-6a661d8e-8ced-4a8c-aba4-e34bc3dde4c1.mp4

After fix:

https://user-images.githubusercontent.com/578608/201521762-13fd869d-aefd-4500-b0ac-e5fe644484c5.mp4