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?
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.
Makarius
_______________________________________________
ProofGeneral mailing list
ProofGeneral@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral
