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

Display instead of pop into Idris repl buffer on startup #588

Closed keram closed 1 year ago

keram commented 1 year ago

Why: To avoid warnings from Idris being displayed in same window as current code buffer on Idris connection and repl startup.

Looking at https://github.com/idris-hackers/idris-mode/issues/380 I think it was always suppose to be display-buffer instead of pop-to-buffer.

Before change:

output-2022-12-09-00:17:04

After change:

output-2022-12-09-00:18:04

If user manualy starts repl with M-x idris-repl the point moves still as expected to the repl.

output-2022-12-09-00:38:17