restrict "bad" markup to command keyword, notably excluding subsequent comments;

--- a/src/Pure/Isar/proof.ML	Mon Jan 14 10:32:33 2013 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Jan 14 13:59:43 2013 +0100
@@ -1030,8 +1030,8 @@
 local
 
 fun skipped_proof state =
-  Context_Position.if_visible (context_of state) Output.report
-    (Markup.markup Markup.bad "Skipped proof");
+  Context_Position.report_text (context_of state) (Position.thread_data ())
+    Markup.bad "Skipped proof";
 
 in