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

Move "words of encouragement" from minibuffer to Idris repl banner #565

Closed keram closed 1 year ago

keram commented 1 year ago

Why: To split concerns of "logging that Idris connection was created" and displaying "words of encouragement for user". To ensure that the words of encouragement are visible to user.

Relates to: https://github.com/idris-hackers/idris-mode/pull/564

After change:

words-encouragement-repl-banner-v2

Messages buffer:

messages-emacs