author | wenzelm |
Tue, 26 Feb 2013 12:50:52 +0100 | |
changeset 51280 | 12b7b0baaa1e |
parent 50298 | 1426d478ccda |
child 51533 | 3f6280aedbcc |
permissions | -rw-r--r-- |
45674 | 1 |
/* Title: Pure/General/time.scala |
45673
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
wenzelm
parents:
45667
diff
changeset
|
2 |
Module: PIDE |
40393 | 3 |
Author: Makarius |
4 |
||
45674 | 5 |
Time based on milliseconds. |
40393 | 6 |
*/ |
7 |
||
8 |
package isabelle |
|
9 |
||
45664 | 10 |
|
50298 | 11 |
import java.util.Locale |
12 |
||
13 |
||
40848
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40393
diff
changeset
|
14 |
object Time |
40393 | 15 |
{ |
47993 | 16 |
def seconds(s: Double): Time = new Time((s * 1000.0).round) |
44699
5199ee17c7d7
property "tooltip-dismiss-delay" is edited in ms, not seconds;
wenzelm
parents:
40852
diff
changeset
|
17 |
def ms(m: Long): Time = new Time(m) |
40393 | 18 |
} |
19 |
||
46712 | 20 |
final class Time private(val ms: Long) |
40848
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40393
diff
changeset
|
21 |
{ |
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40393
diff
changeset
|
22 |
def seconds: Double = ms / 1000.0 |
40852 | 23 |
|
24 |
def min(t: Time): Time = if (ms < t.ms) this else t |
|
25 |
def max(t: Time): Time = if (ms > t.ms) this else t |
|
26 |
||
46768 | 27 |
def is_relevant: Boolean = ms >= 1 |
28 |
||
40848
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40393
diff
changeset
|
29 |
override def toString = |
50298 | 30 |
String.format(Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef]) |
46768 | 31 |
|
40848
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40393
diff
changeset
|
32 |
def message: String = toString + "s" |
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40393
diff
changeset
|
33 |
} |
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40393
diff
changeset
|
34 |