Allow the user to see type errors in mouse-less way about idris-mode HOT 5 CLOSED

notes from IRC:

• display error in minibuffer if point is over an error
• display (optionally) a list of errors in another buffer when C-c C-l finished (also supporting navigation by going up/down the list)
• remove all these buffers and marks at the very start of C-c C-l

from idris-mode.

won't implement the first point in the list, to display when point moves to error:
there's the text-property 'point-entered, which could be used for that, but is not supported for overlays (which we use).
when using a text-property the buffer would be modified, furthermore these persist during copy and paste. not a big fan of doing that (tried and failed)

https://stackoverflow.com/questions/5247377/how-do-i-display-a-prompt-when-the-cursor-enters-an-overlay-in-emacs
http://nflath.com/2010/02/emacs-overlays-and-point-motion/

working on the remaining two items.

from idris-mode.

What's the reason for not implementing in-REPL showing? It's inconvenient to have to jump all around the source to see errors individually.

from idris-mode.

supported in the pull request, just set customization variable idris-warnings-printing to 'warnings-repl ;)
otherwise there is now a tree view of the warnings with navigation to the source!

from idris-mode.

Great, thanks.

from idris-mode.