diff -r 25d6f789618b -r d8c7be27e01d src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Sun Aug 08 14:22:54 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Sun Aug 08 19:36:31 2010 +0200
@@ -24,11 +24,12 @@
     val markup = Map(
       ('A' : Int) -> Markup.INIT,
       ('B' : Int) -> Markup.STATUS,
-      ('C' : Int) -> Markup.WRITELN,
-      ('D' : Int) -> Markup.TRACING,
-      ('E' : Int) -> Markup.WARNING,
-      ('F' : Int) -> Markup.ERROR,
-      ('G' : Int) -> Markup.DEBUG)
+      ('C' : Int) -> Markup.REPORT,
+      ('D' : Int) -> Markup.WRITELN,
+      ('E' : Int) -> Markup.TRACING,
+      ('F' : Int) -> Markup.WARNING,
+      ('G' : Int) -> Markup.ERROR,
+      ('H' : Int) -> Markup.DEBUG)
     def is_raw(kind: String) =
       kind == Markup.STDOUT
     def is_control(kind: String) =
@@ -53,12 +54,13 @@
     def is_control = Kind.is_control(kind)
     def is_system = Kind.is_system(kind)
     def is_status = kind == Markup.STATUS
+    def is_report = kind == Markup.REPORT
     def is_ready = is_status && body == List(XML.Elem(Markup.Ready, Nil))
 
     override def toString: String =
     {
       val res =
-        if (is_status) message.body.map(_.toString).mkString
+        if (is_status || is_report) message.body.map(_.toString).mkString
         else Pretty.string_of(message.body)
       if (properties.isEmpty)
         kind.toString + " [[" + res + "]]"