# HG changeset patch # User wenzelm # Date 1599765290 -7200 # Node ID 13976f92a2d09aef8786352170a598c3a9b5451a # Parent 4bf8a8a2d2adaf30dfe0a1022190eab90f17287f clarified modules; diff -r 4bf8a8a2d2ad -r 13976f92a2d0 src/Pure/ML/ml_statistics.scala --- 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)) } } diff -r 4bf8a8a2d2ad -r 13976f92a2d0 src/Pure/System/java_statistics.scala --- /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) + } +} diff -r 4bf8a8a2d2ad -r 13976f92a2d0 src/Pure/System/platform.scala --- 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) - } } diff -r 4bf8a8a2d2ad -r 13976f92a2d0 src/Pure/build-jars --- 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 diff -r 4bf8a8a2d2ad -r 13976f92a2d0 src/Tools/jEdit/src/status_widget.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()) } })