On 15/12/10 14:33, Makarius wrote:
On Fri, 10 Dec 2010, Michael Chan wrote:
Is there a way to disable the display of messages that are annotated
with proof-shell-eager-annotation-start and
proof-shell-eager-annotation-end? I believe these are so called
Can you explain which messages are getting in the way in particular?
Mostly, the 'Unification bound exceeded' warnings. Exceeding the
unification bound is an expected behaviour in my application, so I think
it should be safe to suppress the warning at times. The main problem is
that my system pretty prints out the tenv and tyenv when it pulls
matchers from a sequence returned by Unify.matchers, but if I get a
warning at a particular matcher, I lose the buffer containing the
The main purpose of "urgent messages" in Proof General is to exchange
certain administrative information between the prover and the editor.
Disabling this is an easy way to mess up the protocol. You should
refrain from touching the protocol channels at all -- at some point
these private system hooks will become inaccesible from user code.
Since the Proof General message model is a bit intricate, i.e. the rules
which kind of messages take precedence over others, there are sometimes
situations where some tools need to emit an urgent message instead of
regular writeln (or tracing) ones. As a consequence such messages take
precedence over everything else, i.e. the trick cannot be repeated by
I see that PG clears the current buffer once it detects a message
annotated with the special characters that prefix a warning message. For
now, I've removed the prefixes and turned a warning message into a
writeln, essentially. No doubt this is not a good way of handling it, so
it'd be great if there's a better way to suppress warning messages.
Postal Address: School of Informatics, University of Edinburgh,
Room 2.05, Informatics Forum, 10 Crichton Street,
Edinburgh EH8 9AB, UK.
Telephone Number: +44-131-651-3077,
Fax Number: +44-131-650-6899,
Web Page: http://homepages.inf.ed.ac.uk/mchan/
ProofGeneral mailing list
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.