By default idris-mode will jump to the last error whenever there is one. I propose adding three options for configuring this behavior: don't jump, jump to first and jump to last.
This jump behavior is probably one of the biggest things interfering with my workflow because I may know very well what error I'm working on, but the idris-mode oftens jumps to very far down in the file.
By default idris-mode will jump to the last error whenever there is one. I propose adding three options for configuring this behavior: don't jump, jump to first and jump to last.
This jump behavior is probably one of the biggest things interfering with my workflow because I may know very well what error I'm working on, but the idris-mode oftens jumps to very far down in the file.