XML.Cache: pipe-lined (thread-safe) version using actor;
tuned Isabelle_Process.pid handling;
--- 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) }
}
--- 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)
--- 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!