tuned signature;
authorwenzelm
Tue Apr 09 20:27:27 2013 +0200 (2013-04-09 ago)
changeset 51663098f3cf6c809
parent 51662 3391a493f39a
child 51664 080ef458f21a
tuned signature;
src/Pure/PIDE/xml.scala
src/Pure/System/isabelle_process.scala
src/Pure/Tools/build.scala
     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  
     2.1 --- a/src/Pure/System/isabelle_process.scala	Tue Apr 09 20:16:52 2013 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.scala	Tue Apr 09 20:27:27 2013 +0200
     2.3 @@ -97,8 +97,7 @@
     2.4      else {
     2.5        val main = XML.Elem(Markup(kind, props), Protocol.clean_message(body))
     2.6        val reports = Protocol.message_reports(props, body)
     2.7 -      for (msg <- main :: reports)
     2.8 -        receiver(new Output(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem]))
     2.9 +      for (msg <- main :: reports) receiver(new Output(xml_cache.elem(msg)))
    2.10      }
    2.11    }
    2.12  
     3.1 --- a/src/Pure/Tools/build.scala	Tue Apr 09 20:16:52 2013 +0200
     3.2 +++ b/src/Pure/Tools/build.scala	Tue Apr 09 20:27:27 2013 +0200
     3.3 @@ -595,7 +595,7 @@
     3.4      val lines = split_lines(text)
     3.5      val xml_cache = new XML.Cache()
     3.6      def parse_lines(prfx: String): List[Properties.T] =
     3.7 -      Props.parse_lines(prfx, lines).map(xml_cache.cache_props)
     3.8 +      Props.parse_lines(prfx, lines).map(xml_cache.props(_))
     3.9  
    3.10      val name =
    3.11        lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) getOrElse ""