1.1 --- a/src/Pure/PIDE/xml.scala	Tue Feb 19 17:55:26 2013 +0100
     1.2 +++ b/src/Pure/PIDE/xml.scala	Tue Feb 19 20:19:21 2013 +0100
     1.3 @@ -188,6 +188,7 @@
     1.4  
     1.5      // main methods
     1.6      def cache_string(x: String): String = synchronized { _cache_string(x) }
     1.7 +    def cache_props(x: Properties.T): Properties.T = synchronized { _cache_props(x) }
     1.8      def cache_markup(x: Markup): Markup = synchronized { _cache_markup(x) }
     1.9      def cache_tree(x: XML.Tree): XML.Tree = synchronized { _cache_tree(x) }
    1.10      def cache_body(x: XML.Body): XML.Body = synchronized { _cache_body(x) }

     2.1 --- a/src/Pure/Tools/build.scala	Tue Feb 19 17:55:26 2013 +0100
     2.2 +++ b/src/Pure/Tools/build.scala	Tue Feb 19 20:19:21 2013 +0100
     2.3 @@ -569,11 +569,15 @@
     2.4    def parse_log(full_stats: Boolean, text: String): Log_Info =
     2.5    {
     2.6      val lines = split_lines(text)
     2.7 +    val xml_cache = new XML.Cache()
     2.8 +    def parse_lines(prfx: String): List[Properties.T] =
     2.9 +      Props.parse_lines(prfx, lines).map(xml_cache.cache_props)
    2.10 +
    2.11      val name =
    2.12        lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) getOrElse ""
    2.13 -    val stats = if (full_stats) Props.parse_lines("\fML_statistics = ", lines) else Nil
    2.14 -    val tasks = if (full_stats) Props.parse_lines("\ftask_statistics = ", lines) else Nil
    2.15 -    val command_timings = Props.parse_lines("\fcommand_timing = ", lines)
    2.16 +    val stats = if (full_stats) parse_lines("\fML_statistics = ") else Nil
    2.17 +    val tasks = if (full_stats) parse_lines("\ftask_statistics = ") else Nil
    2.18 +    val command_timings = parse_lines("\fcommand_timing = ")
    2.19      val session_timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
    2.20      Log_Info(name, stats, tasks, command_timings, session_timing)
    2.21    }