# HG changeset patch
# User wenzelm
# Date 1361301561 -3600
# Node ID c6a8a05ff0a0594ed7dc0aea922652357aa05d7a
# Parent  8c3e5fb411398f8da3d083d8bd690093a8eabff4
help JVM to cope with large symbolic structures;

diff -r 8c3e5fb41139 -r c6a8a05ff0a0 src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Tue Feb 19 17:55:26 2013 +0100
+++ b/src/Pure/PIDE/xml.scala	Tue Feb 19 20:19:21 2013 +0100
@@ -188,6 +188,7 @@
 
     // 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) }
diff -r 8c3e5fb41139 -r c6a8a05ff0a0 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Feb 19 17:55:26 2013 +0100
+++ b/src/Pure/Tools/build.scala	Tue Feb 19 20:19:21 2013 +0100
@@ -569,11 +569,15 @@
   def parse_log(full_stats: Boolean, text: String): Log_Info =
   {
     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)
+
     val name =
       lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) getOrElse ""
-    val stats = if (full_stats) Props.parse_lines("\fML_statistics = ", lines) else Nil
-    val tasks = if (full_stats) Props.parse_lines("\ftask_statistics = ", lines) else Nil
-    val command_timings = Props.parse_lines("\fcommand_timing = ", lines)
+    val stats = if (full_stats) parse_lines("\fML_statistics = ") else Nil
+    val tasks = if (full_stats) parse_lines("\ftask_statistics = ") else Nil
+    val command_timings = parse_lines("\fcommand_timing = ")
     val session_timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
     Log_Info(name, stats, tasks, command_timings, session_timing)
   }