Re: [PG-devel] urgent message hide errors?

2013-02-26 Thread David Aspinall
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 t

Re: [PG-devel] status of support for Proof General

2013-02-26 Thread David Aspinall
Hello Hendrik, It is a good idea to add a note to the trac. I would say that the support is currently by best efforts of people who have other jobs and little spare time -- such as you and I. I think there are other people on this list but probably no very active developers at the moment.

[PG-devel] urgent message hide errors?

2013-02-26 Thread 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

[PG-devel] status of support for Proof General

2013-02-26 Thread Hendrik Tews
Hi, do we have a support problem for Proof General? I am asking because we have issues in the tracker that are quite old and nobody seems to care... for instance #460 or #463 to which I gave partial answers today. Do we have a lack of developers or do the developers not like to comment on issues