store processed content instead of somewhat bulky properties;

--- a/src/Pure/ML/ml_statistics.scala	Wed May 17 14:58:48 2017 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Wed May 17 20:52:24 2017 +0200
@@ -18,17 +18,10 @@
 
 object ML_Statistics
 {
-  /* content interpretation */
+  /* properties */
 
-  final case class Entry(time: Double, data: Map[String, Double])
-  {
-    def heap_size: Long = data.getOrElse("size_heap", 0.0).toLong
-  }
-
-  def apply(ml_statistics: List[Properties.T], heading: String = ""): ML_Statistics =
-    new ML_Statistics(ml_statistics, heading)
-
-  val empty = apply(Nil)
+  val Now = new Properties.Double("now")
+  def now(props: Properties.T): Double = Now.unapply(props).get
 
 
   /* standard fields */
@@ -66,53 +59,70 @@
 
   val main_fields: List[Fields] =
     List(tasks_fields, workers_fields, heap_fields)
+
+
+  /* content interpretation */
+
+  final case class Entry(time: Double, data: Map[String, Double])
+  {
+    def heap_size: Long = data.getOrElse("size_heap", 0.0).toLong
+  }
+
+  val empty: ML_Statistics = apply(Nil)
+
+  def apply(ml_statistics: List[Properties.T], heading: String = ""): ML_Statistics =
+  {
+    require(ml_statistics.forall(props => Now.unapply(props).isDefined))
+
+    val time_start = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.head)
+    val duration = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.last) - time_start
+
+    val fields =
+      SortedSet.empty[String] ++
+        (for (props <- ml_statistics.iterator; (x, _) <- props.iterator if x != Now.name)
+          yield x)
+
+    val content =
+    {
+      var last_edge = Map.empty[String, (Double, Double, Double)]
+      val result = new mutable.ListBuffer[ML_Statistics.Entry]
+      for (props <- ml_statistics) {
+        val time = now(props) - time_start
+        require(time >= 0.0)
+
+        // rising edges -- relative speed
+        val speeds =
+          for ((key, value) <- props; a <- Library.try_unprefix("time", key)) yield {
+            val (x0, y0, s0) = last_edge.getOrElse(a, (0.0, 0.0, 0.0))
+
+            val x1 = time
+            val y1 = java.lang.Double.parseDouble(value)
+            val s1 = if (x1 == x0) 0.0 else (y1 - y0) / (x1 - x0)
+
+            val b = ("speed" + a).intern
+            if (y1 > y0) { last_edge += (a -> (x1, y1, s1)); (b, s1) } else (b, s0)
+          }
+
+        val data =
+          SortedMap.empty[String, Double] ++ speeds ++
+            (for ((x, y) <- props.iterator if x != Now.name)
+              yield (x.intern, java.lang.Double.parseDouble(y)))
+        result += ML_Statistics.Entry(time, data)
+      }
+      result.toList
+    }
+
+    new ML_Statistics(heading, fields, content, time_start, duration)
+  }
 }
 
-final class ML_Statistics private(val ml_statistics: List[Properties.T], val heading: String)
+final class ML_Statistics private(
+  val heading: String,
+  val fields: Set[String],
+  val content: List[ML_Statistics.Entry],
+  val time_start: Double,
+  val duration: Double)
 {
-  val Now = new Properties.Double("now")
-  def now(props: Properties.T): Double = Now.unapply(props).get
-
-  require(ml_statistics.forall(props => Now.unapply(props).isDefined))
-
-  val time_start = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.head)
-  val duration = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.last) - time_start
-
-  val fields: Set[String] =
-    SortedSet.empty[String] ++
-      (for (props <- ml_statistics.iterator; (x, _) <- props.iterator if x != Now.name)
-        yield x)
-
-  val content: List[ML_Statistics.Entry] =
-  {
-    var last_edge = Map.empty[String, (Double, Double, Double)]
-    val result = new mutable.ListBuffer[ML_Statistics.Entry]
-    for (props <- ml_statistics) {
-      val time = now(props) - time_start
-      require(time >= 0.0)
-
-      // rising edges -- relative speed
-      val speeds =
-        for ((key, value) <- props; a <- Library.try_unprefix("time", key)) yield {
-          val (x0, y0, s0) = last_edge.getOrElse(a, (0.0, 0.0, 0.0))
-
-          val x1 = time
-          val y1 = java.lang.Double.parseDouble(value)
-          val s1 = if (x1 == x0) 0.0 else (y1 - y0) / (x1 - x0)
-
-          val b = ("speed" + a).intern
-          if (y1 > y0) { last_edge += (a -> (x1, y1, s1)); (b, s1) } else (b, s0)
-        }
-
-      val data =
-        SortedMap.empty[String, Double] ++ speeds ++
-          (for ((x, y) <- props.iterator if x != Now.name)
-            yield (x, java.lang.Double.parseDouble(y)))
-      result += ML_Statistics.Entry(time, data)
-    }
-    result.toList
-  }
-
   def heap_size_max: Long =
     (0L /: content)({ case (m, entry) => m max entry.heap_size })
 
@@ -154,4 +164,3 @@
         }
       })
 }
-