diff -r 0fe2c01ef7da -r d163f0f28e8c src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Sun Aug 22 12:54:12 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Sun Aug 22 13:52:24 2010 +0200
@@ -95,7 +95,7 @@
 
   private val xml_cache = new XML.Cache(131071)
 
-  private def put_result(kind: String, props: List[(String, String)], body: List[XML.Tree])
+  private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
   {
     if (pid.isEmpty && kind == Markup.INIT)
       pid = props.find(_._1 == Markup.PID).map(_._1)
@@ -257,7 +257,7 @@
       val default_buffer = new Array[Byte](65536)
       var c = -1
 
-      def read_chunk(): List[XML.Tree] =
+      def read_chunk(): XML.Body =
       {
         //{{{
         // chunk size