# HG changeset patch # User wenzelm # Date 1281975636 -7200 # Node ID 9d59dab38feff5acbd96ebe4d17c63d9e5630d0f # Parent ba9ea6b9b75c5d1f4e10dd266cee598c9f331d09 XML.Cache: pipe-lined (thread-safe) version using actor; tuned Isabelle_Process.pid handling; diff -r ba9ea6b9b75c -r 9d59dab38fef src/Pure/General/xml.scala --- a/src/Pure/General/xml.scala Mon Aug 16 17:04:22 2010 +0200 +++ b/src/Pure/General/xml.scala Mon Aug 16 18:20:36 2010 +0200 @@ -10,6 +10,8 @@ import java.lang.ref.WeakReference import javax.xml.parsers.DocumentBuilderFactory +import scala.actors.Actor._ + object XML { @@ -91,66 +93,91 @@ } - /* cache for partial sharing -- NOT THREAD SAFE */ + /* pipe-lined cache for partial sharing */ class Cache(initial_size: Int) { - private val table = new WeakHashMap[Any, WeakReference[Any]](initial_size) - - private def lookup[A](x: A): Option[A] = + private val cache_actor = actor { - val ref = table.get(x) - if (ref == null) None - else { - val y = ref.asInstanceOf[WeakReference[A]].get - if (y == null) None - else Some(y) + val table = new WeakHashMap[Any, WeakReference[Any]](initial_size) + + def lookup[A](x: A): Option[A] = + { + val ref = table.get(x) + if (ref == null) None + else { + val y = ref.asInstanceOf[WeakReference[A]].get + if (y == null) None + else Some(y) + } } - } - private def store[A](x: A): A = - { - table.put(x, new WeakReference[Any](x)) - x - } + def store[A](x: A): A = + { + table.put(x, new WeakReference[Any](x)) + x + } - def cache_string(x: String): String = - lookup(x) match { - case Some(y) => y - case None => store(new String(x.toCharArray)) // trim string value - } - def cache_props(x: List[(String, String)]): List[(String, String)] = - if (x.isEmpty) x - else + def cache_string(x: String): String = + lookup(x) match { + case Some(y) => y + case None => store(new String(x.toCharArray)) // trim string value + } + def cache_props(x: List[(String, String)]): List[(String, String)] = + if (x.isEmpty) x + else + lookup(x) match { + case Some(y) => y + case None => store(x.map(p => (cache_string(p._1), cache_string(p._2)))) + } + def cache_markup(x: Markup): Markup = lookup(x) match { case Some(y) => y - case None => store(x.map(p => (cache_string(p._1), cache_string(p._2)))) + case None => + x match { + case Markup(name, props) => + store(Markup(cache_string(name), cache_props(props))) + } } - def cache_markup(x: Markup): Markup = - lookup(x) match { - case Some(y) => y - case None => - x match { - case Markup(name, props) => - store(Markup(cache_string(name), cache_props(props))) - } - } - def cache_tree(x: XML.Tree): XML.Tree = - lookup(x) match { - case Some(y) => y - case None => - x match { - case XML.Elem(markup, body) => - store(XML.Elem(cache_markup(markup), cache_trees(body))) - case XML.Text(text) => store(XML.Text(cache_string(text))) - } - } - def cache_trees(x: List[XML.Tree]): List[XML.Tree] = - if (x.isEmpty) x - else + def cache_tree(x: XML.Tree): XML.Tree = lookup(x) match { case Some(y) => y - case None => x.map(cache_tree(_)) + case None => + x match { + case XML.Elem(markup, body) => + store(XML.Elem(cache_markup(markup), cache_body(body))) + case XML.Text(text) => store(XML.Text(cache_string(text))) + } } + def cache_body(x: XML.Body): XML.Body = + if (x.isEmpty) x + else + lookup(x) match { + case Some(y) => y + case None => x.map(cache_tree(_)) + } + + // main loop + loop { + react { + case Cache_String(x, f) => f(cache_string(x)) + case Cache_Markup(x, f) => f(cache_markup(x)) + case Cache_Tree(x, f) => f(cache_tree(x)) + case Cache_Body(x, f) => f(cache_body(x)) + case bad => System.err.println("XML.cache_actor: ignoring bad input " + bad) + } + } + } + + private case class Cache_String(x: String, f: String => Unit) + private case class Cache_Markup(x: Markup, f: Markup => Unit) + private case class Cache_Tree(x: XML.Tree, f: XML.Tree => Unit) + private case class Cache_Body(x: XML.Body, f: XML.Body => Unit) + + // main methods + def cache_string(x: String)(f: String => Unit) { cache_actor ! Cache_String(x, f) } + def cache_markup(x: Markup)(f: Markup => Unit) { cache_actor ! Cache_Markup(x, f) } + def cache_tree(x: XML.Tree)(f: XML.Tree => Unit) { cache_actor ! Cache_Tree(x, f) } + def cache_body(x: XML.Body)(f: XML.Body => Unit) { cache_actor ! Cache_Body(x, f) } } diff -r ba9ea6b9b75c -r 9d59dab38fef src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Mon Aug 16 17:04:22 2010 +0200 +++ b/src/Pure/System/isabelle_process.scala Mon Aug 16 18:20:36 2010 +0200 @@ -69,8 +69,6 @@ kind.toString + " " + (for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]" } - - def cache(c: XML.Cache): Result = new Result(c.cache_tree(message).asInstanceOf[XML.Elem]) } } @@ -95,12 +93,15 @@ /* results */ + private val xml_cache = new XML.Cache(131071) + private def put_result(kind: String, props: List[(String, String)], body: List[XML.Tree]) { - if (kind == Markup.INIT) { - for ((Markup.PID, p) <- props) pid = Some(p) - } - receiver ! new Result(XML.Elem(Markup(kind, props), body)) + if (pid.isEmpty && kind == Markup.INIT) + pid = props.find(_._1 == Markup.PID).map(_._1) + + xml_cache.cache_tree(XML.Elem(Markup(kind, props), body))((message: XML.Tree) => + receiver ! new Result(message.asInstanceOf[XML.Elem])) } private def put_result(kind: String, text: String) diff -r ba9ea6b9b75c -r 9d59dab38fef src/Pure/System/session.scala --- a/src/Pure/System/session.scala Mon Aug 16 17:04:22 2010 +0200 +++ b/src/Pure/System/session.scala Mon Aug 16 18:20:36 2010 +0200 @@ -199,8 +199,6 @@ /* main loop */ - val xml_cache = new XML.Cache(131071) - loop { react { case Started(timeout, args) => @@ -223,7 +221,7 @@ handle_change(change) case result: Isabelle_Process.Result => - handle_result(result.cache(xml_cache)) + handle_result(result) case TIMEOUT => // FIXME clarify!