diff -r 25d6f789618b -r d8c7be27e01d src/Pure/General/markup.scala --- a/src/Pure/General/markup.scala Sun Aug 08 14:22:54 2010 +0200 +++ b/src/Pure/General/markup.scala Sun Aug 08 19:36:31 2010 +0200 @@ -196,6 +196,7 @@ val INIT = "init" val STATUS = "status" + val REPORT = "report" val WRITELN = "writeln" val TRACING = "tracing" val WARNING = "warning"