# HG changeset patch
# User wenzelm
# Date 1679167397 -3600
# Node ID 07e2cafcc97ed0963d246a70b023eb6afff34404
# Parent  7969fa41439b8daa0aa7c8f534dd3ad7805b2918
more operations;

diff -r 7969fa41439b -r 07e2cafcc97e 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