src/Pure/PIDE/xml.scala
changeset 51663 098f3cf6c809
parent 51223 c6a8a05ff0a0
child 51987 7d8e0e3c553b
     1.1 --- a/src/Pure/PIDE/xml.scala	Tue Apr 09 20:16:52 2013 +0200
     1.2 +++ b/src/Pure/PIDE/xml.scala	Tue Apr 09 20:27:27 2013 +0200
     1.3 @@ -145,53 +145,54 @@
     1.4  
     1.5      private def trim_bytes(s: String): String = new String(s.toCharArray)
     1.6  
     1.7 -    private def _cache_string(x: String): String =
     1.8 +    private def cache_string(x: String): String =
     1.9        lookup(x) match {
    1.10          case Some(y) => y
    1.11          case None =>
    1.12            val z = trim_bytes(x)
    1.13            if (z.length > max_string) z else store(z)
    1.14        }
    1.15 -    private def _cache_props(x: Properties.T): Properties.T =
    1.16 +    private def cache_props(x: Properties.T): Properties.T =
    1.17        if (x.isEmpty) x
    1.18        else
    1.19          lookup(x) match {
    1.20            case Some(y) => y
    1.21 -          case None => store(x.map(p => (trim_bytes(p._1).intern, _cache_string(p._2))))
    1.22 +          case None => store(x.map(p => (trim_bytes(p._1).intern, cache_string(p._2))))
    1.23          }
    1.24 -    private def _cache_markup(x: Markup): Markup =
    1.25 +    private def cache_markup(x: Markup): Markup =
    1.26        lookup(x) match {
    1.27          case Some(y) => y
    1.28          case None =>
    1.29            x match {
    1.30              case Markup(name, props) =>
    1.31 -              store(Markup(_cache_string(name), _cache_props(props)))
    1.32 +              store(Markup(cache_string(name), cache_props(props)))
    1.33            }
    1.34        }
    1.35 -    private def _cache_tree(x: XML.Tree): XML.Tree =
    1.36 +    private def cache_tree(x: XML.Tree): XML.Tree =
    1.37        lookup(x) match {
    1.38          case Some(y) => y
    1.39          case None =>
    1.40            x match {
    1.41              case XML.Elem(markup, body) =>
    1.42 -              store(XML.Elem(_cache_markup(markup), _cache_body(body)))
    1.43 -            case XML.Text(text) => store(XML.Text(_cache_string(text)))
    1.44 +              store(XML.Elem(cache_markup(markup), cache_body(body)))
    1.45 +            case XML.Text(text) => store(XML.Text(cache_string(text)))
    1.46            }
    1.47        }
    1.48 -    private def _cache_body(x: XML.Body): XML.Body =
    1.49 +    private def cache_body(x: XML.Body): XML.Body =
    1.50        if (x.isEmpty) x
    1.51        else
    1.52          lookup(x) match {
    1.53            case Some(y) => y
    1.54 -          case None => x.map(_cache_tree(_))
    1.55 +          case None => x.map(cache_tree(_))
    1.56          }
    1.57  
    1.58      // main methods
    1.59 -    def cache_string(x: String): String = synchronized { _cache_string(x) }
    1.60 -    def cache_props(x: Properties.T): Properties.T = synchronized { _cache_props(x) }
    1.61 -    def cache_markup(x: Markup): Markup = synchronized { _cache_markup(x) }
    1.62 -    def cache_tree(x: XML.Tree): XML.Tree = synchronized { _cache_tree(x) }
    1.63 -    def cache_body(x: XML.Body): XML.Body = synchronized { _cache_body(x) }
    1.64 +    def string(x: String): String = synchronized { cache_string(x) }
    1.65 +    def props(x: Properties.T): Properties.T = synchronized { cache_props(x) }
    1.66 +    def markup(x: Markup): Markup = synchronized { cache_markup(x) }
    1.67 +    def tree(x: XML.Tree): XML.Tree = synchronized { cache_tree(x) }
    1.68 +    def body(x: XML.Body): XML.Body = synchronized { cache_body(x) }
    1.69 +    def elem(x: XML.Elem): XML.Elem = synchronized { cache_tree(x).asInstanceOf[XML.Elem] }
    1.70    }
    1.71  
    1.72