# HG changeset patch
# User wenzelm
# Date 1679827294 -7200
# Node ID f137bf5d3d94736319111196c77306752c9689ed
# Parent  a6a81f848135c27c210d4650579c47f781382e2c
clarified signature: more explicit types;
tuned output;

diff -r a6a81f848135 -r f137bf5d3d94 src/Pure/General/space.scala
--- 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
diff -r a6a81f848135 -r f137bf5d3d94 src/Pure/ML/ml_statistics.scala
--- 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)
   }
diff -r a6a81f848135 -r f137bf5d3d94 src/Pure/System/java_statistics.scala
--- 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)
   }
 
diff -r a6a81f848135 -r f137bf5d3d94 src/Tools/jEdit/src/status_widget.scala
--- 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 = {