support for Poly/ML memory status;

--- a/src/Pure/ML/ml_statistics.scala	Wed Aug 12 17:53:13 2020 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Wed Aug 12 19:32:45 2020 +0200
@@ -25,6 +25,30 @@
   def now(props: Properties.T): Double = Now.unapply(props).get
 
 
+  /* memory status */
+
+  val Heap_Size = new Properties.Long("size_heap")
+  val Heap_Free = new Properties.Long("size_heap_free_last_GC")
+  val GC_Percent = new Properties.Int("GC_percent")
+
+  sealed case class Memory_Status(heap_size: Long, heap_free: Long, gc_percent: Int)
+  {
+    def heap_used: Long = (heap_size - heap_free) max 0
+    def heap_used_fraction: Double =
+      if (heap_size == 0) 0.0 else heap_used.toDouble / heap_size
+    def gc_progress: Option[Double] =
+      if (1 <= gc_percent && gc_percent <= 100) Some((gc_percent - 1) * 0.01) else None
+  }
+
+  def memory_status(props: Properties.T): Memory_Status =
+  {
+    val heap_size = Heap_Size.get(props)
+    val heap_free = Heap_Free.get(props)
+    val gc_percent = GC_Percent.get(props)
+    Memory_Status(heap_size, heap_free, gc_percent)
+  }
+
+
   /* monitor process */
 
   def monitor(pid: Long,