--- 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: ", " ", "")