# 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
 }