next-error functions: document and streamline

[David Aspinall]

Parsing prover error messages allows more generality in error handling (e.g. dealing with multiple errors, errors in different files).

This has been implemented for Isabelle but not yet documented.

Next error regexps could be combined and some additional output fontification added (to make error regions active). Can we implement this usefully for Coq?

[David Aspinall]

Coq has some custom highlighting for next-error behaviour (I found it had an annoying delay; any user feedback on the feature?). Also, Emacs has its own built-in next-error support which is somewhat generic and could be reused. We should combine all this cleanly.

[courtieu]

One point on this. Error messages of coq are not compliant with next-error syntax. I thought it was simpler to implement a small ad-hos solution.

In future versions of coq there will be a much cleaner xml protocol (equivalent to a very simple version of pgip) and it may be the occasion to switch to a non ad-hoc solution.