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

Great, thanks for trying this.  I agree the change may surprise people
long used to the yellow messages, but it never felt right from the
start.  (Reasons seem a bit lost in the mists of time, I can only
imagine it was to give the user over-excited minibuffer messages during
the progress of the proof).

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

Yes -- more of the same I suspect.  Perhaps excusable if they are
intermittent and not predictable, the excitable warnings are still the
fallback interpretation of these messages.  

Nowadays we're moving to quieter interfaces that keep busy behind the

 - D.

ProofGeneral mailing list

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

Reply via email to