src/Pure/General/timing.scala
changeset 45249 b769a3a370ad
parent 44699 5199ee17c7d7
child 45664 ac6e704dcd12
equal deleted inserted replaced
45248:3b7b64b194ee 45249:b769a3a370ad
    10 {
    10 {
    11   def seconds(s: Double): Time = new Time((s * 1000.0) round)
    11   def seconds(s: Double): Time = new Time((s * 1000.0) round)
    12   def ms(m: Long): Time = new Time(m)
    12   def ms(m: Long): Time = new Time(m)
    13 }
    13 }
    14 
    14 
    15 class Time(val ms: Long)
    15 class Time private(val ms: Long)
    16 {
    16 {
    17   def seconds: Double = ms / 1000.0
    17   def seconds: Double = ms / 1000.0
    18 
    18 
    19   def min(t: Time): Time = if (ms < t.ms) this else t
    19   def min(t: Time): Time = if (ms < t.ms) this else t
    20   def max(t: Time): Time = if (ms > t.ms) this else t
    20   def max(t: Time): Time = if (ms > t.ms) this else t