# HG changeset patch
# User wenzelm
# Date 1357141702 -3600
# Node ID 293e8ec4dfc8ca9ed485e707c7a698b3ef7f01aa
# Parent  12b7e0b4a66ea1680a0d5a1e2ccb8e63ae6b981f
ML runtime statistics: read properties from build log;

diff -r 12b7e0b4a66e -r 293e8ec4dfc8 src/Pure/ML/ml_statistics.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_statistics.scala	Wed Jan 02 16:48:22 2013 +0100
@@ -0,0 +1,41 @@
+/*  Title:      Pure/ML/ml_statistics.ML
+    Author:     Makarius
+
+ML runtime statistics.
+*/
+
+package isabelle
+
+
+object ML_Statistics
+{
+  /* 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)
+}
diff -r 12b7e0b4a66e -r 293e8ec4dfc8 src/Pure/build-jars
--- a/src/Pure/build-jars	Wed Jan 02 15:08:38 2013 +0100
+++ b/src/Pure/build-jars	Wed Jan 02 16:48:22 2013 +0100
@@ -30,6 +30,7 @@
   Isar/outer_syntax.scala
   Isar/parse.scala
   Isar/token.scala
+  ML/ml_statistics.scala
   PIDE/command.scala
   PIDE/document.scala
   PIDE/markup.scala