# 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)