show: display goal refinement rule as "state", to avoid odd Output.urgent_message and make its association with the goal more explicit;

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