src/Pure/System/isabelle_process.scala
changeset 38236 d8c7be27e01d
parent 38231 968844caaff9
child 38253 3d4e521014f7
     1.1 --- a/src/Pure/System/isabelle_process.scala	Sun Aug 08 14:22:54 2010 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Sun Aug 08 19:36:31 2010 +0200
     1.3 @@ -24,11 +24,12 @@
     1.4      val markup = Map(
     1.5        ('A' : Int) -> Markup.INIT,
     1.6        ('B' : Int) -> Markup.STATUS,
     1.7 -      ('C' : Int) -> Markup.WRITELN,
     1.8 -      ('D' : Int) -> Markup.TRACING,
     1.9 -      ('E' : Int) -> Markup.WARNING,
    1.10 -      ('F' : Int) -> Markup.ERROR,
    1.11 -      ('G' : Int) -> Markup.DEBUG)
    1.12 +      ('C' : Int) -> Markup.REPORT,
    1.13 +      ('D' : Int) -> Markup.WRITELN,
    1.14 +      ('E' : Int) -> Markup.TRACING,
    1.15 +      ('F' : Int) -> Markup.WARNING,
    1.16 +      ('G' : Int) -> Markup.ERROR,
    1.17 +      ('H' : Int) -> Markup.DEBUG)
    1.18      def is_raw(kind: String) =
    1.19        kind == Markup.STDOUT
    1.20      def is_control(kind: String) =
    1.21 @@ -53,12 +54,13 @@
    1.22      def is_control = Kind.is_control(kind)
    1.23      def is_system = Kind.is_system(kind)
    1.24      def is_status = kind == Markup.STATUS
    1.25 +    def is_report = kind == Markup.REPORT
    1.26      def is_ready = is_status && body == List(XML.Elem(Markup.Ready, Nil))
    1.27  
    1.28      override def toString: String =
    1.29      {
    1.30        val res =
    1.31 -        if (is_status) message.body.map(_.toString).mkString
    1.32 +        if (is_status || is_report) message.body.map(_.toString).mkString
    1.33          else Pretty.string_of(message.body)
    1.34        if (properties.isEmpty)
    1.35          kind.toString + " [[" + res + "]]"