--- a/src/Pure/General/space.scala Fri Mar 24 18:30:17 2023 +0000
+++ b/src/Pure/General/space.scala Sun Mar 26 12:41:34 2023 +0200
@@ -36,6 +36,10 @@
def is_proper: Boolean = bytes > 0
def is_relevant: Boolean = MiB >= 1.0
+ def used(free: Space): Space = new Space((bytes - free.bytes) max 0)
+ def used_fraction(free: Space): Double =
+ if (is_proper && used(free).is_proper) used(free).B / B else 0.0
+
def B: Double = bytes.toDouble
def KiB: Double = B / 1024
def MiB: Double = KiB / 1024
--- a/src/Pure/ML/ml_statistics.scala Fri Mar 24 18:30:17 2023 +0000
+++ b/src/Pure/ML/ml_statistics.scala Sun Mar 26 12:41:34 2023 +0200
@@ -30,17 +30,16 @@
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
+ sealed case class Memory_Status(heap_size: Space, heap_free: Space, gc_percent: Int) {
+ def heap_used: Space = heap_size.used(heap_free)
+ def heap_used_fraction: Double = heap_size.used_fraction(heap_free)
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 heap_size = Space.bytes(Heap_Size.get(props))
+ val heap_free = Space.bytes(Heap_Free.get(props))
val gc_percent = GC_Percent.get(props)
Memory_Status(heap_size, heap_free, gc_percent)
}
--- a/src/Pure/System/java_statistics.scala Fri Mar 24 18:30:17 2023 +0000
+++ b/src/Pure/System/java_statistics.scala Sun Mar 26 12:41:34 2023 +0200
@@ -10,15 +10,14 @@
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
+ sealed case class Memory_Status(heap_size: Space, heap_free: Space) {
+ def heap_used: Space = heap_size.used(heap_free)
+ def heap_used_fraction: Double = heap_size.used_fraction(heap_free)
}
def memory_status(): Memory_Status = {
- val heap_size = Runtime.getRuntime.totalMemory()
- val heap_free = Runtime.getRuntime.freeMemory()
+ val heap_size = Space.bytes(Runtime.getRuntime.totalMemory())
+ val heap_free = Space.bytes(Runtime.getRuntime.freeMemory())
Memory_Status(heap_size, heap_free)
}
--- a/src/Tools/jEdit/src/status_widget.scala Fri Mar 24 18:30:17 2023 +0000
+++ b/src/Tools/jEdit/src/status_widget.scala Sun Mar 26 12:41:34 2023 +0200
@@ -104,8 +104,8 @@
private var status = Java_Statistics.memory_status()
def get_status: (String, Double) = {
- ("JVM: " + (status.heap_used / 1024 / 1024) + "/" + (status.heap_size / 1024 / 1024) + "MB",
- status.heap_used_fraction)
+ val text = "JVM: " + status.heap_used.MiB.round + "/" + status.heap_size.MiB.round + "MiB"
+ (text, status.heap_used_fraction)
}
private def update_status(new_status: Java_Statistics.Memory_Status): Unit = {
@@ -160,8 +160,8 @@
status.gc_progress match {
case Some(p) => ("ML cleanup", 1.0 - p)
case None =>
- ("ML: " + (status.heap_used / 1024 / 1024) + "/" + (status.heap_size / 1024 / 1024) + "MB",
- status.heap_used_fraction)
+ val text = "ML: " + status.heap_used.MiB.round + "/" + status.heap_size.MiB.round + "MiB"
+ (text, status.heap_used_fraction)
}
private def update_status(new_status: ML_Statistics.Memory_Status): Unit = {