# HG changeset patch
# User wenzelm
# Date 1358168383 -3600
# Node ID f3588e59aeaa64b454be4d2e2f3bc4e8fe3c905a
# Parent  e6317e8b11dbfccb5ec498e95b6b0263331e94b5
restrict "bad" markup to command keyword, notably excluding subsequent comments;

diff -r e6317e8b11db -r f3588e59aeaa src/Pure/Isar/proof.ML
--- 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