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