# HG changeset patch
# User wenzelm
# Date 1310392590 -7200
# Node ID 74a9e9c8d5e85f2577994e0ff6f05cacdd508128
# Parent  a41f618c641d531bd797e0d9d07875b7b486fa9f
tuned signature;

diff -r a41f618c641d -r 74a9e9c8d5e8 src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Mon Jul 11 11:13:33 2011 +0200
+++ b/src/Pure/General/xml.scala	Mon Jul 11 15:56:30 2011 +0200
@@ -72,11 +72,14 @@
 
   def content_stream(tree: Tree): Stream[String] =
     tree match {
-      case Elem(_, body) => body.toStream.flatten(content_stream(_))
+      case Elem(_, body) => content_stream(body)
       case Text(content) => Stream(content)
     }
+  def content_stream(body: Body): Stream[String] =
+    body.toStream.flatten(content_stream(_))
 
   def content(tree: Tree): Iterator[String] = content_stream(tree).iterator
+  def content(body: Body): Iterator[String] = content_stream(body).iterator
 
 
   /* pipe-lined cache for partial sharing */
diff -r a41f618c641d -r 74a9e9c8d5e8 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Mon Jul 11 11:13:33 2011 +0200
+++ b/src/Pure/System/isabelle_process.scala	Mon Jul 11 15:56:30 2011 +0200
@@ -45,9 +45,9 @@
 
   class Result(val message: XML.Elem) extends Message
   {
-    def kind = message.markup.name
-    def properties = message.markup.properties
-    def body = message.body
+    def kind: String = message.markup.name
+    def properties: XML.Attributes = message.markup.properties
+    def body: XML.Body = message.body
 
     def is_init = kind == Markup.INIT
     def is_exit = kind == Markup.EXIT