clarified modules;

--- a/src/Pure/ML/ml_statistics.scala	Thu Sep 10 21:07:58 2020 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Thu Sep 10 21:14:50 2020 +0200
@@ -99,7 +99,7 @@
     private def consume(props: Properties.T): Unit = synchronized
     {
       if (session != null) {
-        val props1 = (session.xml_cache.props(props ::: Platform.jvm_statistics()))
+        val props1 = (session.xml_cache.props(props ::: Java_Statistics.jvm_statistics()))
         session.runtime_statistics.post(Session.Runtime_Statistics(props1))
       }
     }

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/java_statistics.scala	Thu Sep 10 21:14:50 2020 +0200
@@ -0,0 +1,45 @@
+/*  Title:      Pure/System/java_statistics.scala
+    Author:     Makarius
+
+Java runtime statistics.
+*/
+
+package isabelle
+
+
+object Java_Statistics
+{
+  /* memory status */
+
+  sealed case class Memory_Status(heap_size: Long, heap_free: Long)
+  {
+    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 memory_status(): Memory_Status =
+  {
+    val heap_size = Runtime.getRuntime.totalMemory()
+    val heap_used = heap_size - Runtime.getRuntime.freeMemory()
+    Memory_Status(heap_size, heap_used)
+  }
+
+
+  /* JVM statistics */
+
+  def jvm_statistics(): Properties.T =
+  {
+    val status = memory_status()
+    val threads = Thread.activeCount()
+    val workers = Isabelle_Thread.pool.getPoolSize
+    val workers_active = Isabelle_Thread.pool.getActiveCount
+
+    List(
+      "java_heap_size" -> status.heap_size.toString,
+      "java_heap_used" -> status.heap_used.toString,
+      "java_threads_total" -> threads.toString,
+      "java_workers_total" -> workers.toString,
+      "java_workers_active" -> workers_active.toString)
+  }
+}

--- a/src/Pure/System/platform.scala	Thu Sep 10 21:07:58 2020 +0200
+++ b/src/Pure/System/platform.scala	Thu Sep 10 21:14:50 2020 +0200
@@ -68,39 +68,4 @@
   /* JVM name */
 
   val jvm_name: String = System.getProperty("java.vm.name", "")
-
-
-  /* memory status */
-
-  sealed case class Memory_Status(heap_size: Long, heap_free: Long)
-  {
-    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 memory_status(): Memory_Status =
-  {
-    val heap_size = Runtime.getRuntime.totalMemory()
-    val heap_used = heap_size - Runtime.getRuntime.freeMemory()
-    Memory_Status(heap_size, heap_used)
-  }
-
-
-  /* JVM statistics */
-
-  def jvm_statistics(): Properties.T =
-  {
-    val status = memory_status()
-    val threads = Thread.activeCount()
-    val workers = Isabelle_Thread.pool.getPoolSize
-    val workers_active = Isabelle_Thread.pool.getActiveCount
-
-    List(
-      "java_heap_size" -> status.heap_size.toString,
-      "java_heap_used" -> status.heap_used.toString,
-      "java_threads_total" -> threads.toString,
-      "java_workers_total" -> workers.toString,
-      "java_workers_active" -> workers_active.toString)
-  }
 }

--- a/src/Pure/build-jars	Thu Sep 10 21:07:58 2020 +0200
+++ b/src/Pure/build-jars	Thu Sep 10 21:14:50 2020 +0200
@@ -126,6 +126,7 @@
   src/Pure/System/isabelle_process.scala
   src/Pure/System/isabelle_system.scala
   src/Pure/System/isabelle_tool.scala
+  src/Pure/System/java_statistics.scala
   src/Pure/System/linux.scala
   src/Pure/System/numa.scala
   src/Pure/System/options.scala

--- a/src/Tools/jEdit/src/status_widget.scala	Thu Sep 10 21:07:58 2020 +0200
+++ b/src/Tools/jEdit/src/status_widget.scala	Thu Sep 10 21:14:50 2020 +0200
@@ -106,7 +106,7 @@
   {
     /* component state -- owned by GUI thread */
 
-    private var status = Platform.memory_status()
+    private var status = Java_Statistics.memory_status()
 
     def get_status: (String, Double) =
     {
@@ -114,7 +114,7 @@
         status.heap_used_fraction)
     }
 
-    private def update_status(new_status: Platform.Memory_Status)
+    private def update_status(new_status: Java_Statistics.Memory_Status)
     {
       if (status != new_status) {
         status = new_status
@@ -128,7 +128,7 @@
     private val timer =
       new Timer(500, new ActionListener {
         override def actionPerformed(e: ActionEvent) {
-          update_status(Platform.memory_status())
+          update_status(Java_Statistics.memory_status())
         }
       })