--- 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)
+ })
+}
+