support JVM runtime statistics;

--- a/src/Pure/ML/ml_statistics.scala	Thu Aug 13 14:41:28 2020 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Thu Aug 13 15:11:30 2020 +0200
@@ -99,8 +99,8 @@
     private def consume(props: Properties.T): Unit = synchronized
     {
       if (session != null) {
-        val stats = Session.Runtime_Statistics(session.xml_cache.props(props))
-        session.runtime_statistics.post(stats)
+        val props1 = (session.xml_cache.props(props ::: Platform.jvm_statistics()))
+        session.runtime_statistics.post(Session.Runtime_Statistics(props1))
       }
     }
 
@@ -172,12 +172,21 @@
 
   private val time_speed = Map("time_CPU" -> "speed_CPU", "time_GC" -> "speed_GC")
 
+  val java_heap_fields: Fields =
+    ("Java heap", List("java_heap_size", "java_heap_used"))
+
+  val java_thread_fields: Fields =
+    ("Java threads", List("java_threads_total", "java_workers_total", "java_workers_active"))
+
 
   val main_fields: List[Fields] =
     List(heap_fields, tasks_fields, workers_fields)
 
-  val all_fields: List[Fields] =
-    main_fields ::: List(threads_fields, GC_fields, program_fields, time_fields, speed_fields)
+  val other_fields: List[Fields] =
+    List(threads_fields, GC_fields, program_fields, time_fields, speed_fields,
+      java_heap_fields, java_thread_fields)
+
+  val all_fields: List[Fields] = main_fields ::: other_fields
 
 
   /* content interpretation */

--- a/src/Pure/System/platform.scala	Thu Aug 13 14:41:28 2020 +0200
+++ b/src/Pure/System/platform.scala	Thu Aug 13 15:11:30 2020 +0200
@@ -68,4 +68,24 @@
   /* JVM name */
 
   val jvm_name: String = System.getProperty("java.vm.name", "")
+
+
+  /* JVM statistics */
+
+  def jvm_statistics(): Properties.T =
+  {
+    val heap_size = Runtime.getRuntime.totalMemory()
+    val heap_used = heap_size - Runtime.getRuntime.freeMemory()
+
+    val threads = Thread.activeCount()
+    val workers = Isabelle_Thread.pool.getPoolSize
+    val workers_active = Isabelle_Thread.pool.getActiveCount
+
+    List(
+      "java_heap_size" -> heap_size.toString,
+      "java_heap_used" -> heap_used.toString,
+      "java_threads_total" -> threads.toString,
+      "java_workers_total" -> workers.toString,
+      "java_workers_active" -> workers_active.toString)
+  }
 }