synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
authorwenzelm
Sun Sep 04 19:06:45 2011 +0200 (2011-09-04 ago)
changeset 44704528d635ef6f0
parent 44703 f2bfe19239bc
child 44705 089fcaf94c00
synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
src/Pure/PIDE/xml.scala
     1.1 --- a/src/Pure/PIDE/xml.scala	Sun Sep 04 17:50:19 2011 +0200
     1.2 +++ b/src/Pure/PIDE/xml.scala	Sun Sep 04 19:06:45 2011 +0200
     1.3 @@ -89,94 +89,74 @@
     1.4  
     1.5    class Cache(initial_size: Int = 131071, max_string: Int = 100)
     1.6    {
     1.7 -    private val cache_actor = actor
     1.8 -    {
     1.9 -      val table = new WeakHashMap[Any, WeakReference[Any]](initial_size)
    1.10 +    private var table = new WeakHashMap[Any, WeakReference[Any]](initial_size)
    1.11  
    1.12 -      def lookup[A](x: A): Option[A] =
    1.13 -      {
    1.14 -        val ref = table.get(x)
    1.15 -        if (ref == null) None
    1.16 -        else {
    1.17 -          val y = ref.asInstanceOf[WeakReference[A]].get
    1.18 -          if (y == null) None
    1.19 -          else Some(y)
    1.20 -        }
    1.21 -      }
    1.22 -      def store[A](x: A): A =
    1.23 -      {
    1.24 -        table.put(x, new WeakReference[Any](x))
    1.25 -        x
    1.26 +    private def lookup[A](x: A): Option[A] =
    1.27 +    {
    1.28 +      val ref = table.get(x)
    1.29 +      if (ref == null) None
    1.30 +      else {
    1.31 +        val y = ref.asInstanceOf[WeakReference[A]].get
    1.32 +        if (y == null) None
    1.33 +        else Some(y)
    1.34        }
    1.35 +    }
    1.36 +    private def store[A](x: A): A =
    1.37 +    {
    1.38 +      table.put(x, new WeakReference[Any](x))
    1.39 +      x
    1.40 +    }
    1.41  
    1.42 -      def trim_bytes(s: String): String = new String(s.toCharArray)
    1.43 +    private def trim_bytes(s: String): String = new String(s.toCharArray)
    1.44  
    1.45 -      def cache_string(x: String): String =
    1.46 -        lookup(x) match {
    1.47 -          case Some(y) => y
    1.48 -          case None =>
    1.49 -            val z = trim_bytes(x)
    1.50 -            if (z.length > max_string) z else store(z)
    1.51 -        }
    1.52 -      def cache_props(x: Properties.T): Properties.T =
    1.53 -        if (x.isEmpty) x
    1.54 -        else
    1.55 -          lookup(x) match {
    1.56 -            case Some(y) => y
    1.57 -            case None => store(x.map(p => (trim_bytes(p._1).intern, cache_string(p._2))))
    1.58 -          }
    1.59 -      def cache_markup(x: Markup): Markup =
    1.60 +    private def _cache_string(x: String): String =
    1.61 +      lookup(x) match {
    1.62 +        case Some(y) => y
    1.63 +        case None =>
    1.64 +          val z = trim_bytes(x)
    1.65 +          if (z.length > max_string) z else store(z)
    1.66 +      }
    1.67 +    private def _cache_props(x: Properties.T): Properties.T =
    1.68 +      if (x.isEmpty) x
    1.69 +      else
    1.70          lookup(x) match {
    1.71            case Some(y) => y
    1.72 -          case None =>
    1.73 -            x match {
    1.74 -              case Markup(name, props) =>
    1.75 -                store(Markup(cache_string(name), cache_props(props)))
    1.76 -            }
    1.77 +          case None => store(x.map(p => (trim_bytes(p._1).intern, _cache_string(p._2))))
    1.78          }
    1.79 -      def cache_tree(x: XML.Tree): XML.Tree =
    1.80 +    private def _cache_markup(x: Markup): Markup =
    1.81 +      lookup(x) match {
    1.82 +        case Some(y) => y
    1.83 +        case None =>
    1.84 +          x match {
    1.85 +            case Markup(name, props) =>
    1.86 +              store(Markup(_cache_string(name), _cache_props(props)))
    1.87 +          }
    1.88 +      }
    1.89 +    private def _cache_tree(x: XML.Tree): XML.Tree =
    1.90 +      lookup(x) match {
    1.91 +        case Some(y) => y
    1.92 +        case None =>
    1.93 +          x match {
    1.94 +            case XML.Elem(markup, body) =>
    1.95 +              store(XML.Elem(_cache_markup(markup), _cache_body(body)))
    1.96 +            case XML.Text(text) => store(XML.Text(_cache_string(text)))
    1.97 +          }
    1.98 +      }
    1.99 +    private def _cache_body(x: XML.Body): XML.Body =
   1.100 +      if (x.isEmpty) x
   1.101 +      else
   1.102          lookup(x) match {
   1.103            case Some(y) => y
   1.104 -          case None =>
   1.105 -            x match {
   1.106 -              case XML.Elem(markup, body) =>
   1.107 -                store(XML.Elem(cache_markup(markup), cache_body(body)))
   1.108 -              case XML.Text(text) => store(XML.Text(cache_string(text)))
   1.109 -            }
   1.110 +          case None => x.map(_cache_tree(_))
   1.111          }
   1.112 -      def cache_body(x: XML.Body): XML.Body =
   1.113 -        if (x.isEmpty) x
   1.114 -        else
   1.115 -          lookup(x) match {
   1.116 -            case Some(y) => y
   1.117 -            case None => x.map(cache_tree(_))
   1.118 -          }
   1.119 -
   1.120 -      // main loop
   1.121 -      loop {
   1.122 -        react {
   1.123 -          case Cache_String(x, f) => f(cache_string(x))
   1.124 -          case Cache_Markup(x, f) => f(cache_markup(x))
   1.125 -          case Cache_Tree(x, f) => f(cache_tree(x))
   1.126 -          case Cache_Body(x, f) => f(cache_body(x))
   1.127 -          case Cache_Ignore(x, f) => f(x)
   1.128 -          case bad => System.err.println("XML.cache_actor: ignoring bad input " + bad)
   1.129 -        }
   1.130 -      }
   1.131 -    }
   1.132 -
   1.133 -    private case class Cache_String(x: String, f: String => Unit)
   1.134 -    private case class Cache_Markup(x: Markup, f: Markup => Unit)
   1.135 -    private case class Cache_Tree(x: XML.Tree, f: XML.Tree => Unit)
   1.136 -    private case class Cache_Body(x: XML.Body, f: XML.Body => Unit)
   1.137 -    private case class Cache_Ignore[A](x: A, f: A => Unit)
   1.138  
   1.139      // main methods
   1.140 -    def cache_string(x: String)(f: String => Unit) { cache_actor ! Cache_String(x, f) }
   1.141 -    def cache_markup(x: Markup)(f: Markup => Unit) { cache_actor ! Cache_Markup(x, f) }
   1.142 -    def cache_tree(x: XML.Tree)(f: XML.Tree => Unit) { cache_actor ! Cache_Tree(x, f) }
   1.143 -    def cache_body(x: XML.Body)(f: XML.Body => Unit) { cache_actor ! Cache_Body(x, f) }
   1.144 -    def cache_ignore[A](x: A)(f: A => Unit) { cache_actor ! Cache_Ignore(x, f) }
   1.145 +    // FIXME simplify signatures
   1.146 +    def cache_string(x: String)(f: String => Unit): Unit = f(synchronized { _cache_string(x) })
   1.147 +    def cache_markup(x: Markup)(f: Markup => Unit): Unit = f(synchronized { _cache_markup(x) })
   1.148 +    def cache_tree(x: XML.Tree)(f: XML.Tree => Unit): Unit = f(synchronized { _cache_tree(x) })
   1.149 +    def cache_body(x: XML.Body)(f: XML.Body => Unit): Unit = f(synchronized { _cache_body(x) })
   1.150 +    def cache_ignore[A](x: A)(f: A => Unit): Unit = f(x)
   1.151    }
   1.152  
   1.153