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?

Michael, I'm also interested to hear the answer to this.

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.

Yes: on that note, I have been meaning to ask on the Isabelle devel list if we can remove the "[Successful|Failed] attempt to solve goal by ..." message from having the urgent message classification.

I don't think it is important to the protocol, but rather it should be classified as a goals type of message and appear in that display. I don't understand why it was ever marked as being urgent, except (I suppose) for the side effect of giving some progress reporting for nested proofs. But its appearing in another buffer always confused me and it doesn't work well with the decorated scripts (mouse hovers with goals buffer output) in PG 4.0.

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.

Yes, except to clarify that all of the urgent messages will be processed, so this is a way to ensure that messages are dealt with by the interface rather than ignored.

See doc of `proof-shell-filter' in PG adapting manual,


 - D.

ProofGeneral mailing list

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Reply via email to