more compact ML_Statistics, to make build_status work with less than 2GB heap;

--- a/src/Pure/Admin/build_status.scala	Sat Mar 03 17:37:33 2018 +0100
+++ b/src/Pure/Admin/build_status.scala	Sat Mar 03 21:38:27 2018 +0100
@@ -57,9 +57,14 @@
     ml_statistics: Boolean = false,
     image_size: (Int, Int) = default_image_size)
   {
+    val ml_statistics_domain =
+      Iterator(ML_Statistics.heap_fields, ML_Statistics.tasks_fields, ML_Statistics.workers_fields).
+        flatMap(_._2).toSet
+
     val data =
       read_data(options, progress = progress, profiles = profiles,
-        only_sessions = only_sessions, ml_statistics = ml_statistics, verbose = verbose)
+        only_sessions = only_sessions, verbose = verbose,
+        ml_statistics = ml_statistics, ml_statistics_domain = ml_statistics_domain)
 
     present_data(data, progress = progress, target_dir = target_dir, image_size = image_size)
   }
@@ -187,6 +192,7 @@
     profiles: List[Profile] = default_profiles,
     only_sessions: Set[String] = Set.empty,
     ml_statistics: Boolean = false,
+    ml_statistics_domain: String => Boolean = (key: String) => true,
     verbose: Boolean = false): Data =
   {
     val date = Date.now()
@@ -269,6 +275,7 @@
                 if (ml_statistics)
                   Properties.uncompress(res.bytes(Build_Log.Data.ml_statistics))
                 else Nil,
+                domain = ml_statistics_domain,
                 heading = session_name + print_version(isabelle_version, afp_version, chapter))
 
             val entry =

--- a/src/Pure/ML/ml_statistics.scala	Sat Mar 03 17:37:33 2018 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Sat Mar 03 21:38:27 2018 +0100
@@ -79,7 +79,8 @@
 
   val empty: ML_Statistics = apply(Nil)
 
-  def apply(ml_statistics: List[Properties.T], heading: String = ""): ML_Statistics =
+  def apply(ml_statistics: List[Properties.T], heading: String = "",
+    domain: String => Boolean = (key: String) => true): ML_Statistics =
   {
     require(ml_statistics.forall(props => Now.unapply(props).isDefined))
 
@@ -88,8 +89,10 @@
 
     val fields =
       SortedSet.empty[String] ++
-        (for (props <- ml_statistics.iterator; (x, _) <- props.iterator if x != Now.name)
-          yield x)
+        (for {
+          props <- ml_statistics.iterator
+          (x, _) <- props.iterator
+          if x != Now.name && domain(x) } yield x)
 
     val content =
     {
@@ -101,24 +104,32 @@
 
         // rising edges -- relative speed
         val speeds =
-          for ((key, value) <- props; a <- Library.try_unprefix("time", key)) yield {
+          (for {
+            (key, value) <- props.iterator
+            a <- Library.try_unprefix("time", key)
+            b = "speed" + a if domain(b)
+          }
+          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)
-          }
+            if (y1 > y0) {
+              last_edge += (a -> (x1, y1, s1))
+              (b, s1.toString)
+            }
+            else (b, s0.toString)
+          }).toList
 
         val data =
-          SortedMap.empty[String, Double] ++ speeds ++
-            (for ((x, y) <- props.iterator if x != Now.name)
-             yield {
-               val z = java.lang.Double.parseDouble(y)
-              (x.intern, if (heap_fields._2.contains(x)) heap_scale(z) else z)
-            })
+          SortedMap.empty[String, Double] ++
+            (for {
+              (x, y) <- props.iterator ++ speeds.iterator
+              if x != Now.name && domain(x)
+              z = java.lang.Double.parseDouble(y) if z != 0.0
+            } yield { (x.intern, if (heap_fields._2.contains(x)) heap_scale(z) else z) })
 
         result += ML_Statistics.Entry(time, data)
       }
@@ -170,7 +181,7 @@
       field <- selected_fields.iterator
       series = new XYSeries(field)
     } {
-      content.foreach(entry => series.add(entry.time, entry.data(field)))
+      content.foreach(entry => series.add(entry.time, entry.get(field)))
       data.addSeries(series)
     }
   }