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 _______________________________________________ ProofGeneral-devel mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
