src/Pure/System/isabelle_process.scala
changeset 38573 d163f0f28e8c
parent 38446 9d59dab38fef
child 38636 b7647ca7de5a
     1.1 --- a/src/Pure/System/isabelle_process.scala	Sun Aug 22 12:54:12 2010 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Sun Aug 22 13:52:24 2010 +0200
     1.3 @@ -95,7 +95,7 @@
     1.4  
     1.5    private val xml_cache = new XML.Cache(131071)
     1.6  
     1.7 -  private def put_result(kind: String, props: List[(String, String)], body: List[XML.Tree])
     1.8 +  private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
     1.9    {
    1.10      if (pid.isEmpty && kind == Markup.INIT)
    1.11        pid = props.find(_._1 == Markup.PID).map(_._1)
    1.12 @@ -257,7 +257,7 @@
    1.13        val default_buffer = new Array[Byte](65536)
    1.14        var c = -1
    1.15  
    1.16 -      def read_chunk(): List[XML.Tree] =
    1.17 +      def read_chunk(): XML.Body =
    1.18        {
    1.19          //{{{
    1.20          // chunk size