tuned signature;
authorwenzelm
Mon Jul 11 15:56:30 2011 +0200 (2011-07-11)
changeset 4374774a9e9c8d5e8
parent 43746 a41f618c641d
child 43748 c70bd78ec83c
tuned signature;
src/Pure/General/xml.scala
src/Pure/System/isabelle_process.scala
     1.1 --- a/src/Pure/General/xml.scala	Mon Jul 11 11:13:33 2011 +0200
     1.2 +++ b/src/Pure/General/xml.scala	Mon Jul 11 15:56:30 2011 +0200
     1.3 @@ -72,11 +72,14 @@
     1.4  
     1.5    def content_stream(tree: Tree): Stream[String] =
     1.6      tree match {
     1.7 -      case Elem(_, body) => body.toStream.flatten(content_stream(_))
     1.8 +      case Elem(_, body) => content_stream(body)
     1.9        case Text(content) => Stream(content)
    1.10      }
    1.11 +  def content_stream(body: Body): Stream[String] =
    1.12 +    body.toStream.flatten(content_stream(_))
    1.13  
    1.14    def content(tree: Tree): Iterator[String] = content_stream(tree).iterator
    1.15 +  def content(body: Body): Iterator[String] = content_stream(body).iterator
    1.16  
    1.17  
    1.18    /* pipe-lined cache for partial sharing */
     2.1 --- a/src/Pure/System/isabelle_process.scala	Mon Jul 11 11:13:33 2011 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.scala	Mon Jul 11 15:56:30 2011 +0200
     2.3 @@ -45,9 +45,9 @@
     2.4  
     2.5    class Result(val message: XML.Elem) extends Message
     2.6    {
     2.7 -    def kind = message.markup.name
     2.8 -    def properties = message.markup.properties
     2.9 -    def body = message.body
    2.10 +    def kind: String = message.markup.name
    2.11 +    def properties: XML.Attributes = message.markup.properties
    2.12 +    def body: XML.Body = message.body
    2.13  
    2.14      def is_init = kind == Markup.INIT
    2.15      def is_exit = kind == Markup.EXIT