Error highlighting

[ElifUskuplu]

I've added an error highlighting property to proofgeneral mode. However, this is incomplete. It captures error position well, but in highlight, there is some shifting problem for some cases. An example is below.

I assume this is due to special characters. I'm working on this, but I wanted to show its current situation.

[ElifUskuplu]

I updated error highlight clearing rules, but I've found another problem in highlighting. If there is a line break between last successful span and the line containing the error, highlighting shifts accordingly.

[remimimimimi]

Wouldn't it be a better idea to use ready-made libraries for error highlighting like flymake-mode or flycheck-mode? See comparison here. I think flycheck-mode will be a better fit, since it should be easier to work with.

[mikeshulman]

@remimimimimi Thanks for the suggestion! I've never used either of those, but my impression (possibly erroneous) is that they wouldn't be a great fit. They seem designed to run a syntax checker themselves, asynchronously in the background on the entire buffer, and parse its pre-existing output format. Whereas in our situation, ProofGeneral is already handling the invocation of and communication with the proof assistant, which is synchronous and executes only one command at a time, plus we can also customize the output of the proof assistant to make it trivially easy to parse. Possibly there are some pieces of those packages that we could use, but I'm doubtful that trying to do so would save us more work than it created. But if you think differently, please explain!

[ElifUskuplu]

@remimimimimi I agree with Mike. Also, I'm not sure whether using them both flycheck and proofgeneral together can cause some problems. I've no experience with the former.

[mikeshulman]

I did a bit of quick google searching and didn't turn up anyone combining flycheck+proofgeneral.

[remimimimimi]

I recommended looking at them because it seemed strange that the proof general doesn’t handle overlays itself. It seemed like a solution for this, but agree that flycheck solving different problem.

Rocq seems to implement their own error highlighting mechanism as well. I checked proof general code base to find where error highlighting could happen automatically from error regex, but found nothing.

Want to mention that proof general has predefined faces for error highlighting proof-script-sticky-error-face and proof-script-highlight-error-face, which you might want to use instead of creating your own. Also, you don’t have to store overlays in variable, as you can delete all overlays in range by their face property like this (remove-overlays beg end 'face 'narya-error-face).

[mikeshulman]

Thanks for the tips! Maybe we should look at the Rocq code for some ideas, then.

I think the immediate reason for the offset shift is that the current code is counting offsets from the end of the last successful span rather than the beginning of the current unsuccessful span, and PG skips past blank lines (at least) before starting to grab the current command that it sends to the PA, so those two are not the same. There must be a way to grab the current span even in the case of an error.

[mikeshulman]

This PR needed merging with master, and while I was looking at it I found a way to fix the issue. Weirdly proof-action-list is set to nil in the case of an error before the handle-output function is called, but we can grab the correct starting location by advising proof-shell-error-or-interrupt-action. I also fixed a few things in the code for clearing error highlights.