--- 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 */
--- 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