# HG changeset patch
# User wenzelm
# Date 1365532047 -7200
# Node ID 098f3cf6c809d9619cadfe5b8af78ba0373e2acc
# Parent  3391a493f39a7a10bedece602b553a639ea8143d
tuned signature;

diff -r 3391a493f39a -r 098f3cf6c809 src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Tue Apr 09 20:16:52 2013 +0200
+++ b/src/Pure/PIDE/xml.scala	Tue Apr 09 20:27:27 2013 +0200
@@ -145,53 +145,54 @@
 
     private def trim_bytes(s: String): String = new String(s.toCharArray)
 
-    private def _cache_string(x: String): String =
+    private def cache_string(x: String): String =
       lookup(x) match {
         case Some(y) => y
         case None =>
           val z = trim_bytes(x)
           if (z.length > max_string) z else store(z)
       }
-    private def _cache_props(x: Properties.T): Properties.T =
+    private def cache_props(x: Properties.T): Properties.T =
       if (x.isEmpty) x
       else
         lookup(x) match {
           case Some(y) => y
-          case None => store(x.map(p => (trim_bytes(p._1).intern, _cache_string(p._2))))
+          case None => store(x.map(p => (trim_bytes(p._1).intern, cache_string(p._2))))
         }
-    private def _cache_markup(x: Markup): Markup =
+    private 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)))
+              store(Markup(cache_string(name), cache_props(props)))
           }
       }
-    private def _cache_tree(x: XML.Tree): XML.Tree =
+    private 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_body(body)))
-            case XML.Text(text) => store(XML.Text(_cache_string(text)))
+              store(XML.Elem(cache_markup(markup), cache_body(body)))
+            case XML.Text(text) => store(XML.Text(cache_string(text)))
           }
       }
-    private def _cache_body(x: XML.Body): XML.Body =
+    private 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(_))
+          case None => x.map(cache_tree(_))
         }
 
     // main methods
-    def cache_string(x: String): String = synchronized { _cache_string(x) }
-    def cache_props(x: Properties.T): Properties.T = synchronized { _cache_props(x) }
-    def cache_markup(x: Markup): Markup = synchronized { _cache_markup(x) }
-    def cache_tree(x: XML.Tree): XML.Tree = synchronized { _cache_tree(x) }
-    def cache_body(x: XML.Body): XML.Body = synchronized { _cache_body(x) }
+    def string(x: String): String = synchronized { cache_string(x) }
+    def props(x: Properties.T): Properties.T = synchronized { cache_props(x) }
+    def markup(x: Markup): Markup = synchronized { cache_markup(x) }
+    def tree(x: XML.Tree): XML.Tree = synchronized { cache_tree(x) }
+    def body(x: XML.Body): XML.Body = synchronized { cache_body(x) }
+    def elem(x: XML.Elem): XML.Elem = synchronized { cache_tree(x).asInstanceOf[XML.Elem] }
   }
 
 
diff -r 3391a493f39a -r 098f3cf6c809 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Tue Apr 09 20:16:52 2013 +0200
+++ b/src/Pure/System/isabelle_process.scala	Tue Apr 09 20:27:27 2013 +0200
@@ -97,8 +97,7 @@
     else {
       val main = XML.Elem(Markup(kind, props), Protocol.clean_message(body))
       val reports = Protocol.message_reports(props, body)
-      for (msg <- main :: reports)
-        receiver(new Output(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem]))
+      for (msg <- main :: reports) receiver(new Output(xml_cache.elem(msg)))
     }
   }
 
diff -r 3391a493f39a -r 098f3cf6c809 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Apr 09 20:16:52 2013 +0200
+++ b/src/Pure/Tools/build.scala	Tue Apr 09 20:27:27 2013 +0200
@@ -595,7 +595,7 @@
     val lines = split_lines(text)
     val xml_cache = new XML.Cache()
     def parse_lines(prfx: String): List[Properties.T] =
-      Props.parse_lines(prfx, lines).map(xml_cache.cache_props)
+      Props.parse_lines(prfx, lines).map(xml_cache.props(_))
 
     val name =
       lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) getOrElse ""