diff -r 5a9964f7a691 -r 20126dd9772c src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Jan 08 19:02:12 2013 +0100
+++ b/src/Pure/Tools/build.scala	Tue Jan 08 21:16:51 2013 +0100
@@ -509,7 +509,7 @@
   }
 
 
-  /* log files and corresponding heaps */
+  /* log files */
 
   private val LOG = Path.explode("log")
   private def log(name: String): Path = LOG + Path.basic(name)
@@ -517,6 +517,19 @@
 
   private val SESSION_PARENT_PATH = "\fSession.parent_path = "
 
+  sealed case class Log_Info(stats: List[Properties.T], timing: Properties.T)
+
+  def parse_log(text: String): Log_Info =
+  {
+    val lines = split_lines(text)
+    val stats = Properties.parse_lines("\fML_statistics = ", lines)
+    val timing = Properties.find_parse_line("\fTiming = ", lines) getOrElse Nil
+    Log_Info(stats, timing)
+  }
+
+
+  /* sources and heaps */
+
   private def sources_stamp(digests: List[SHA1.Digest]): String =
     digests.map(_.toString).sorted.mkString("sources: ", " ", "")