1.1 --- a/src/Pure/ML/ml_statistics.scala	Wed Jan 02 18:03:38 2013 +0100
     1.2 +++ b/src/Pure/ML/ml_statistics.scala	Wed Jan 02 19:23:18 2013 +0100
     1.3 @@ -7,6 +7,9 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 +import scala.collection.immutable.{SortedSet, SortedMap}
     1.8 +
     1.9 +
    1.10  object ML_Statistics
    1.11  {
    1.12    /* read properties from build log */
    1.13 @@ -38,4 +41,38 @@
    1.14        if line.startsWith(line_prefix)
    1.15        stats = line.substring(line_prefix.length)
    1.16      } yield Parser.parse_stats(stats)
    1.17 +
    1.18 +
    1.19 +  /* content interpretation */
    1.20 +
    1.21 +  val Now = new Properties.Double("now")
    1.22 +  final case class Entry(time: Double, data: Map[String, Double])
    1.23 +
    1.24 +  def apply(stats: List[Properties.T]): ML_Statistics = new ML_Statistics(stats)
    1.25 +  def apply(log: Path): ML_Statistics = apply(read_log(log))
    1.26  }
    1.27 +
    1.28 +final class ML_Statistics private(val stats: List[Properties.T])
    1.29 +{
    1.30 +  require(!stats.isEmpty && stats.forall(props => ML_Statistics.Now.unapply(props).isDefined))
    1.31 +
    1.32 +  val time_start = ML_Statistics.Now.unapply(stats.head).get
    1.33 +  val duration = ML_Statistics.Now.unapply(stats.last).get - time_start
    1.34 +
    1.35 +  val names: Set[String] =
    1.36 +    SortedSet.empty[String] ++
    1.37 +      (for (props <- stats.iterator; (x, _) <- props.iterator if x != ML_Statistics.Now.name)
    1.38 +        yield x)
    1.39 +
    1.40 +  val content: List[ML_Statistics.Entry] =
    1.41 +    stats.map(props => {
    1.42 +      val time = ML_Statistics.Now.unapply(props).get - time_start
    1.43 +      require(time >= 0.0)
    1.44 +      val data =
    1.45 +        SortedMap.empty[String, Double] ++
    1.46 +          (for ((x, y) <- props.iterator if x != ML_Statistics.Now.name)
    1.47 +            yield (x, java.lang.Double.parseDouble(y)))
    1.48 +      ML_Statistics.Entry(time, data)
    1.49 +    })
    1.50 +}
    1.51 +