On Wed, 15 Dec 2010, David Aspinall wrote:

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.

This is an ancient workaround to get some output to the user in a proof state. When checking again about urgent messages some weeks ago, I've asked myself if that is still required.

In Isabelle/9240be8c8c69 this message is now printed as a goal state. There are still a few weeks until the release, to see if there are any surprises due to this change after so many years.

Many other uses of urgent messages in user code in HOL are less clear.


        Makarius
_______________________________________________
ProofGeneral mailing list
ProofGeneral@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral

Reply via email to