src/Pure/PIDE/markup.ML
changeset 64677 8dc24130e8fe
parent 63806 c54a53ef1873
child 65313 347ed6219dab
--- a/src/Pure/PIDE/markup.ML	Tue Dec 27 17:33:57 2016 +0100
+++ b/src/Pure/PIDE/markup.ML	Wed Dec 28 10:39:50 2016 +0100
@@ -173,7 +173,7 @@
   val protocolN: string
   val reportN: string val report: T
   val no_reportN: string val no_report: T
-  val badN: string val bad: T
+  val badN: string val bad: unit -> T
   val intensifyN: string val intensify: T
   val browserN: string
   val graphviewN: string
@@ -573,7 +573,8 @@
 val (reportN, report) = markup_elem "report";
 val (no_reportN, no_report) = markup_elem "no_report";
 
-val (badN, bad) = markup_elem "bad";
+val badN = "bad";
+fun bad () = (badN, serial_properties (serial ()));
 
 val (intensifyN, intensify) = markup_elem "intensify";