urgent message hide errors?

[Hendrik Tews]

Hi,

currently, proof-shell-filter looks for urgent messages before
looking for errors. Moreover, if an urgent message is found, it
searches for errors only in the output that follows the urgent
message.

This behavior is responsible for issue #463, where Coq outputs an
error before a warning and the error is lost because the warning
is recognized as urgent message.

What is the problem here? Coq outputting the warning _after_ the
error? Or matching the warning as urgent message? Or searching
for errors only behind urgent messages?

Bye,

Hendrik

[David Aspinall]

Post by Hendrik Tews
What is the problem here? Coq outputting the warning _after_ the
error? Or matching the warning as urgent message? Or searching
for errors only behind urgent messages?

From Proof General's point of view, the first of these is the problem,
since the behaviour has been well specified for a long time and I guess
that Coq's behaviour has changed over time. See fragment of
documentation from proof-shell-filter below.

- David


Error or interrupt messages are expected to terminate an
interactive output and appear last before a prompt and will
always be processed. Error messages and interrupt messages are
therefore *not* considered as urgent messages.


see:

http://proofgeneral.inf.ed.ac.uk/htmlshow.php?title=Proof+General+adapting+manual&file=releases%2FProofGeneral%2Fdoc%2FPG-adapting%2FPG-adapting_15.html#index-proof_002dshell_002dfilter