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