diff -r 177b90f33f40 -r 00e8b836d4db src/Pure/ML/ml_statistics.scala --- a/src/Pure/ML/ml_statistics.scala Thu May 18 14:14:20 2017 +0200 +++ b/src/Pure/ML/ml_statistics.scala Thu May 18 14:38:09 2017 +0200 @@ -25,10 +25,16 @@ def now(props: Properties.T): Double = Now.unapply(props).get - /* standard fields */ + /* heap */ val HEAP_SIZE = "size_heap" + def heap_scale(x: Long): Long = x / 1024 / 1024 + def heap_scale(x: Double): Double = heap_scale(x.toLong).toLong + + + /* standard fields */ + type Fields = (String, List[String]) val tasks_fields: Fields = @@ -109,7 +115,11 @@ val data = SortedMap.empty[String, Double] ++ speeds ++ (for ((x, y) <- props.iterator if x != Now.name) - yield (x.intern, java.lang.Double.parseDouble(y))) + yield { + val z = java.lang.Double.parseDouble(y) + (x.intern, if (heap_fields._2.contains(x)) heap_scale(z) else z) + }) + result += ML_Statistics.Entry(time, data) } result.toList