| changeset 47993 | 135fd6f2dadd |
| parent 46768 | 46acd255810d |
| child 50298 | 1426d478ccda |
| 47992:7700f0e9618c | 47993:135fd6f2dadd |
|---|---|
8 package isabelle |
8 package isabelle |
9 |
9 |
10 |
10 |
11 object Time |
11 object Time |
12 { |
12 { |
13 def seconds(s: Double): Time = new Time((s * 1000.0) round) |
13 def seconds(s: Double): Time = new Time((s * 1000.0).round) |
14 def ms(m: Long): Time = new Time(m) |
14 def ms(m: Long): Time = new Time(m) |
15 } |
15 } |
16 |
16 |
17 final class Time private(val ms: Long) |
17 final class Time private(val ms: Long) |
18 { |
18 { |