# HG changeset patch # User wenzelm # Date 1292442740 -3600 # Node ID 9240be8c8c69e16d044a3cd9a585a02cff8d99c6 # Parent a99bc6f3664b230b5e667d83225fa99bd1ba8b26 show: display goal refinement rule as "state", to avoid odd Output.urgent_message and make its association with the goal more explicit; diff -r a99bc6f3664b -r 9240be8c8c69 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Wed Dec 15 19:41:24 2010 +0100 +++ b/src/Pure/Isar/proof.ML Wed Dec 15 20:52:20 2010 +0100 @@ -993,7 +993,8 @@ if ! testing then () else Proof_Display.print_results int ctxt res; fun print_rule ctxt th = if ! testing then rule := SOME th - else if int then Output.urgent_message (Proof_Display.string_of_rule ctxt "Successful" th) + else if int then + writeln (Markup.markup Markup.state (Proof_Display.string_of_rule ctxt "Successful" th)) else (); val test_proof = try (local_skip_proof true)