src/Pure/ML/ml_statistics.scala

 */
 
 package isabelle
 
 
+import scala.annotation.tailrec
 import scala.collection.mutable
 import scala.collection.immutable.{SortedSet, SortedMap}
 import scala.swing.{Frame, Component}
 
 import org.jfree.data.xy.{XYSeries, XYSeriesCollection}

   def now(props: Properties.T): Double = Now.unapply(props).get
 
 
   /* standard fields */
 
+  val HEAP_SIZE = "size_heap"
+
   type Fields = (String, Iterable[String])
 
   val tasks_fields: Fields =
     ("Future tasks",
       List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive", "tasks_urgent"))

 
   val GC_fields: Fields =
     ("GCs", List("partial_GCs", "full_GCs"))
 
   val heap_fields: Fields =
-    ("Heap", List("size_heap", "size_allocation", "size_allocation_free",
+    ("Heap", List(HEAP_SIZE, "size_allocation", "size_allocation_free",
       "size_heap_free_last_full_GC", "size_heap_free_last_GC"))
 
   val threads_fields: Fields =
     ("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar",
       "threads_wait_IO", "threads_wait_mutex", "threads_wait_signal"))

 
   /* content interpretation */
 
   final case class Entry(time: Double, data: Map[String, Double])
   {
-    def heap_size: Long = data.getOrElse("size_heap", 0.0).toLong
+    def get(field: String): Double = data.getOrElse(field, 0.0)
   }
 
   val empty: ML_Statistics = apply(Nil)
 
   def apply(ml_statistics: List[Properties.T], heading: String = ""): ML_Statistics =

   val fields: Set[String],
   val content: List[ML_Statistics.Entry],
   val time_start: Double,
   val duration: Double)
 {
-  def heap_size_max: Long =
-    (0L /: content)({ case (m, entry) => m max entry.heap_size })
+  /* content */
+
+  def maximum(field: String): Double =
+    (0.0 /: content)({ case (m, e) => m max e.get(field) })
+
+  def average(field: String): Double =
+  {
+    @tailrec def sum(t0: Double, list: List[ML_Statistics.Entry], acc: Double): Double =
+      list match {
+        case Nil => acc
+        case e :: es =>
+          val t = e.time
+          sum(t, es, (t - t0) * e.get(field) + acc)
+      }
+    content match {
+      case Nil => 0.0
+      case List(e) => e.get(field)
+      case e :: es => sum(e.time, es, 0.0) / duration
+    }
+  }
+
+  def maximum_heap_size: Long = maximum(ML_Statistics.HEAP_SIZE).toLong
+  def average_heap_size: Long = average(ML_Statistics.HEAP_SIZE).toLong
 
 
   /* charts */
 
   def update_data(data: XYSeriesCollection, selected_fields: Iterable[String])