--- a/src/Pure/General/space.scala Sat Jan 28 15:38:36 2023 +0100
+++ b/src/Pure/General/space.scala Sat Jan 28 16:06:38 2023 +0100
@@ -28,6 +28,9 @@
}
final class Space private(val bytes: Long) extends AnyVal {
+ def is_proper: Boolean = bytes > 0
+ def is_relevant: Boolean = MiB >= 1.0
+
def B: Double = bytes.toDouble
def KiB: Double = B / 1024
def MiB: Double = KiB / 1024
@@ -48,4 +51,6 @@
print_unit(bytes.toDouble, Space.units)
}
+
+ def print_relevant: Option[String] = if (is_relevant) Some(print) else None
}