src/Pure/General/space.scala
changeset 77694 ea509b0bfc80
parent 77687 07e2cafcc97e
child 77708 f137bf5d3d94
equal deleted inserted replaced
77693:068ff989c143 77694:ea509b0bfc80
    29 
    29 
    30 final class Space private(val bytes: Long) extends AnyVal {
    30 final class Space private(val bytes: Long) extends AnyVal {
    31   def + (other: Space): Space = new Space(bytes + other.bytes)
    31   def + (other: Space): Space = new Space(bytes + other.bytes)
    32   def - (other: Space): Space = new Space(bytes - other.bytes)
    32   def - (other: Space): Space = new Space(bytes - other.bytes)
    33   def * (scalar: Double): Space = new Space((bytes * scalar).round)
    33   def * (scalar: Double): Space = new Space((bytes * scalar).round)
       
    34   def / (other: Space): Double = B / other.B
    34 
    35 
    35   def is_proper: Boolean = bytes > 0
    36   def is_proper: Boolean = bytes > 0
    36   def is_relevant: Boolean = MiB >= 1.0
    37   def is_relevant: Boolean = MiB >= 1.0
    37 
    38 
    38   def B: Double = bytes.toDouble
    39   def B: Double = bytes.toDouble