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
'urgent messages'.

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 previous output.

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
other tools.

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,
Email: m.c...@ed.ac.uk
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.

Reply via email to