src/Pure/General/space.scala

--- a/src/Pure/General/space.scala	Fri Mar 17 11:24:52 2023 +0000
+++ b/src/Pure/General/space.scala	Sat Mar 18 20:23:17 2023 +0100
@@ -28,6 +28,10 @@
 }
 
 final class Space private(val bytes: Long) extends AnyVal {
+  def + (other: Space): Space = new Space(bytes + other.bytes)
+  def - (other: Space): Space = new Space(bytes - other.bytes)
+  def * (scalar: Double): Space = new Space((bytes * scalar).round)
+
   def is_proper: Boolean = bytes > 0
   def is_relevant: Boolean = MiB >= 1.0