diff -r cf24cc0b0a47 -r db070951dfee src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Wed May 17 13:52:46 2017 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Wed May 17 14:58:48 2017 +0200
@@ -21,6 +21,9 @@
   /* content interpretation */
 
   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)
@@ -110,6 +113,9 @@
     result.toList
   }
 
+  def heap_size_max: Long =
+    (0L /: content)({ case (m, entry) => m max entry.heap_size })
+
 
   /* charts */