--- 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 */