merged

--- a/src/Pure/General/space.scala	Fri Mar 17 13:56:54 2023 +0100
+++ b/src/Pure/General/space.scala	Sat Mar 18 23:48:56 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