src/Pure/General/markup.ML
changeset 39171 525a13b9ac74
parent 39168 e3ac771235f7
child 39439 1c294d150ded
--- a/src/Pure/General/markup.ML	Tue Sep 07 15:03:59 2010 +0200
+++ b/src/Pure/General/markup.ML	Tue Sep 07 16:08:29 2010 +0200
@@ -120,6 +120,7 @@
   val promptN: string val prompt: T
   val readyN: string val ready: T
   val reportN: string val report: T
+  val badN: string val bad: T
   val no_output: output * output
   val default_output: T -> output * output
   val add_mode: string -> (T -> output * output) -> unit
@@ -348,6 +349,8 @@
 
 val (reportN, report) = markup_elem "report";
 
+val (badN, bad) = markup_elem "bad";
+
 
 
 (** print mode operations **)