src/Pure/System/isabelle_process.scala
changeset 38446 9d59dab38fef
parent 38445 ba9ea6b9b75c
child 38573 d163f0f28e8c
     1.1 --- a/src/Pure/System/isabelle_process.scala	Mon Aug 16 17:04:22 2010 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Mon Aug 16 18:20:36 2010 +0200
     1.3 @@ -69,8 +69,6 @@
     1.4          kind.toString + " " +
     1.5            (for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
     1.6      }
     1.7 -
     1.8 -    def cache(c: XML.Cache): Result = new Result(c.cache_tree(message).asInstanceOf[XML.Elem])
     1.9    }
    1.10  }
    1.11  
    1.12 @@ -95,12 +93,15 @@
    1.13  
    1.14    /* results */
    1.15  
    1.16 +  private val xml_cache = new XML.Cache(131071)
    1.17 +
    1.18    private def put_result(kind: String, props: List[(String, String)], body: List[XML.Tree])
    1.19    {
    1.20 -    if (kind == Markup.INIT) {
    1.21 -      for ((Markup.PID, p) <- props) pid = Some(p)
    1.22 -    }
    1.23 -    receiver ! new Result(XML.Elem(Markup(kind, props), body))
    1.24 +    if (pid.isEmpty && kind == Markup.INIT)
    1.25 +      pid = props.find(_._1 == Markup.PID).map(_._1)
    1.26 +
    1.27 +    xml_cache.cache_tree(XML.Elem(Markup(kind, props), body))((message: XML.Tree) =>
    1.28 +      receiver ! new Result(message.asInstanceOf[XML.Elem]))
    1.29    }
    1.30  
    1.31    private def put_result(kind: String, text: String)