diff -r 5a9964f7a691 -r 20126dd9772c src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Tue Jan 08 19:02:12 2013 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Tue Jan 08 21:16:51 2013 +0100
@@ -22,7 +22,7 @@
   final case class Entry(time: Double, data: Map[String, Double])
 
   def apply(stats: List[Properties.T]): ML_Statistics = new ML_Statistics(stats)
-  def apply(log: Path): ML_Statistics = apply(read_log(log))
+  def apply(path: Path): ML_Statistics = apply(Build.parse_log(File.read_gzip(path)).stats)
 
   val empty = apply(Nil)
 
@@ -50,37 +50,6 @@
 
   val standard_fields =
     List(GC_fields, heap_fields, threads_fields, time_fields, tasks_fields, workers_fields)
-
-
-  /* read properties from build log */
-
-  private val line_prefix = "\fML_statistics = "
-
-  private val syntax = Outer_Syntax.empty + "," + "(" + ")" + "[" + "]"
-
-  private object Parser extends Parse.Parser
-  {
-    private def stat: Parser[(String, String)] =
-      keyword("(") ~ string ~ keyword(",") ~ string ~ keyword(")") ^^
-      { case _ ~ x ~ _ ~ y ~ _ => (x, y) }
-    private def stats: Parser[Properties.T] =
-      keyword("[") ~> repsep(stat, keyword(",")) <~ keyword("]")
-
-    def parse_stats(s: String): Properties.T =
-    {
-      parse_all(stats, Token.reader(syntax.scan(s))) match {
-        case Success(result, _) => result
-        case bad => error(bad.toString)
-      }
-    }
-  }
-
-  def read_log(log: Path): List[Properties.T] =
-    for {
-      line <- split_lines(File.read_gzip(log))
-      if line.startsWith(line_prefix)
-      stats = line.substring(line_prefix.length)
-    } yield Parser.parse_stats(stats)
 }
 
 final class ML_Statistics private(val stats: List[Properties.T])