# HG changeset patch # User wenzelm # Date 1674918398 -3600 # Node ID 8c14be9beb58fa603e100942317ebaa8d61a471b # Parent 34a6b8bd7abd804df7a0a24a8ba3f2ba4f973ae4 more operations; diff -r 34a6b8bd7abd -r 8c14be9beb58 src/Pure/General/space.scala --- 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 }