--- 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)
- }
}