There's an option you can find using M-x customize-group RET idris2 RET:

Hide Idris2 Stay In Current Window On Compiler Error: Toggle  on (non-nil)
    State : SAVED and set.
   Stay in current window if type checking fails.

I think it may be off by default.

I like my emacs to be minimally noisy so I turned it on (and turned "Hole Show On Load" off)
but I don't know how popular these settings are compared to the defaults.

@gallais Thanks! Didn't even think to check if this behaviour was on purpose and controlled by an option. :)

Unfortunately, while setting idris2-stay-in-current-window-on-compiler-error prevents the error window from stealing the focus immediately, it still moves my cursor to the beginning of the line, and – worse – still steals the focus when I type any non-character.

Here's an example where I run idris2-load-file in a buffer after introducing an error (deleting an >) and where the cursor first jumps to the beginning of the line, and then, when I fix the issue by typing an >, the cursor jumps to the *idris2-notes* window:

Hi @ehamberg can you please try if the same strange behaviour is present when using https://github.com/idris-hackers/idris-mode ?
I wasn't able reproduce this issue but is also possible that the idris mode doesn't play well with some other package you have installed.
Can you test if the behaviour is present also when other packages are disabled (especially company mode)?

@keram:

can you please try if the same strange behaviour is present when using https://github.com/idris-hackers/idris-mode ?

It is not. The *idris-notes* initially steals the focus, but when I move it back to my file buffer, it stays there, and I can fix the error(s) without the focus jumping back to *idris-notes*.

Can you test if the behaviour is present also when other packages are disabled (especially company mode)?

Whoa, if I disable company-mode in the buffer, the focus-stealing stops! (The cursor still jumps to the beginning of the line, but that's the only weird behaviour left after disabling company-mode and setting idris2-stay-in-current-window-on-compiler-error to t.)

It's not the first time company-mode seems to interact badly with the idris2-mode 😩

ehamberg commented [14 hours ago]
The cursor still jumps to the beginning of the line, but that's the only weird behaviour left

Thank you @ehamberg
That is indeed still weird 🤔

gallais commented 1 hour ago
It's not the first time company-mode seems to interact badly with the idris2-mode 😩

It may be worth to add to readme steps to disable it for idris mode buffers.
Sounds like interesting issue to figure out but I myself I'm not user of company mode

It may be worth to add to readme steps to disable it for idris mode buffers. Sounds like interesting issue to figure out but I myself I'm not user of company mode

Yep. This seems to work:

(setq company-global-modes '(not idris2-mode))

I am seeing the same thing using corfu. *Messages* notes that:

Debugger entered--Lisp error: (error "I can't make sense of the completion task:\n--eval ...")
  error("%s (synchronous Idris2 evaluation failed)" "I can't make sense of the completion task:\n--eval ...")
  funcall(error "%s (synchronous Idris2 evaluation failed)" "I can't make sense of the completion task:\n--eval ...")
  apply(funcall (error "%s (synchronous Idris2 evaluation failed)" "I can't make sense of the completion task:\n--eval ..."))
  idris2-eval((:repl-completions "--eval (LiftIO "))
  idris2-complete-at-point()

I feel it might be better to ignore the failed evaluation rather than pass it on. Preparing a PR