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.

ProofGeneral mailing list

Reply via email to