src/Pure/System/isabelle_process.scala
changeset 43746 a41f618c641d
parent 43745 562e35bc351e
child 43747 74a9e9c8d5e8
     1.1 --- a/src/Pure/System/isabelle_process.scala	Mon Jul 11 10:27:50 2011 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Mon Jul 11 11:13:33 2011 +0200
     1.3 @@ -29,7 +29,8 @@
     1.4        ('D' : Int) -> Markup.WRITELN,
     1.5        ('E' : Int) -> Markup.TRACING,
     1.6        ('F' : Int) -> Markup.WARNING,
     1.7 -      ('G' : Int) -> Markup.ERROR)
     1.8 +      ('G' : Int) -> Markup.ERROR,
     1.9 +      ('H' : Int) -> Markup.RAW)
    1.10    }
    1.11  
    1.12    abstract class Message
    1.13 @@ -54,6 +55,7 @@
    1.14      def is_system = kind == Markup.SYSTEM
    1.15      def is_status = kind == Markup.STATUS
    1.16      def is_report = kind == Markup.REPORT
    1.17 +    def is_raw = kind == Markup.RAW
    1.18      def is_ready = Isar_Document.is_ready(message)
    1.19      def is_syslog = is_init || is_exit || is_system || is_ready
    1.20  
    1.21 @@ -95,9 +97,13 @@
    1.22    private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
    1.23    {
    1.24      if (kind == Markup.INIT) rm_fifos()
    1.25 -    val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
    1.26 -    xml_cache.cache_tree(msg)((message: XML.Tree) =>
    1.27 -      receiver ! new Result(message.asInstanceOf[XML.Elem]))
    1.28 +    if (kind == Markup.RAW)
    1.29 +      receiver ! new Result(XML.Elem(Markup(kind, props), body))
    1.30 +    else {
    1.31 +      val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
    1.32 +      xml_cache.cache_tree(msg)((message: XML.Tree) =>
    1.33 +        receiver ! new Result(message.asInstanceOf[XML.Elem]))
    1.34 +    }
    1.35    }
    1.36  
    1.37    private def put_result(kind: String, text: String)
    1.38 @@ -324,7 +330,7 @@
    1.39        val default_buffer = new Array[Byte](65536)
    1.40        var c = -1
    1.41  
    1.42 -      def read_chunk(): XML.Body =
    1.43 +      def read_chunk(decode: Boolean): XML.Body =
    1.44        {
    1.45          //{{{
    1.46          // chunk size
    1.47 @@ -351,19 +357,24 @@
    1.48  
    1.49          if (i != n) throw new Protocol_Error("bad message chunk content")
    1.50  
    1.51 -        YXML.parse_body_failsafe(YXML.decode_chars(Symbol.decode, buf, 0, n))
    1.52 +        if (decode)
    1.53 +          YXML.parse_body_failsafe(Standard_System.decode_chars(Symbol.decode, buf, 0, n))
    1.54 +        else List(XML.Text(Standard_System.decode_chars(s => s, buf, 0, n).toString))
    1.55          //}}}
    1.56        }
    1.57  
    1.58        do {
    1.59          try {
    1.60 -          val header = read_chunk()
    1.61 -          val body = read_chunk()
    1.62 +          val header = read_chunk(true)
    1.63            header match {
    1.64              case List(XML.Elem(Markup(name, props), Nil))
    1.65                  if name.size == 1 && Kind.message_markup.isDefinedAt(name(0)) =>
    1.66 -              put_result(Kind.message_markup(name(0)), props, body)
    1.67 -            case _ => throw new Protocol_Error("bad header: " + header.toString)
    1.68 +              val kind = Kind.message_markup(name(0))
    1.69 +              val body = read_chunk(kind != Markup.RAW)
    1.70 +              put_result(kind, props, body)
    1.71 +            case _ =>
    1.72 +              read_chunk(false)
    1.73 +              throw new Protocol_Error("bad header: " + header.toString)
    1.74            }
    1.75          }
    1.76          catch {