# HG changeset patch
# User wenzelm
# Date 1357150998 -3600
# Node ID f02864682307d52de4c5204af9f55c1dadf073a9
# Parent  a8db4bf70e9009ac8e390ff15f3a2a7dfded5ff7
some support for ML statistics content interpretation;

diff -r a8db4bf70e90 -r f02864682307 src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Wed Jan 02 18:03:38 2013 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Wed Jan 02 19:23:18 2013 +0100
@@ -7,6 +7,9 @@
 package isabelle
 
 
+import scala.collection.immutable.{SortedSet, SortedMap}
+
+
 object ML_Statistics
 {
   /* read properties from build log */
@@ -38,4 +41,38 @@
       if line.startsWith(line_prefix)
       stats = line.substring(line_prefix.length)
     } yield Parser.parse_stats(stats)
+
+
+  /* content interpretation */
+
+  val Now = new Properties.Double("now")
+  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))
 }
+
+final class ML_Statistics private(val stats: List[Properties.T])
+{
+  require(!stats.isEmpty && stats.forall(props => ML_Statistics.Now.unapply(props).isDefined))
+
+  val time_start = ML_Statistics.Now.unapply(stats.head).get
+  val duration = ML_Statistics.Now.unapply(stats.last).get - time_start
+
+  val names: Set[String] =
+    SortedSet.empty[String] ++
+      (for (props <- stats.iterator; (x, _) <- props.iterator if x != ML_Statistics.Now.name)
+        yield x)
+
+  val content: List[ML_Statistics.Entry] =
+    stats.map(props => {
+      val time = ML_Statistics.Now.unapply(props).get - time_start
+      require(time >= 0.0)
+      val data =
+        SortedMap.empty[String, Double] ++
+          (for ((x, y) <- props.iterator if x != ML_Statistics.Now.name)
+            yield (x, java.lang.Double.parseDouble(y)))
+      ML_Statistics.Entry(time, data)
+    })
+}
+