author | wenzelm |
Tue, 07 Apr 2020 21:49:36 +0200 | |
changeset 71726 | a5fda30edae2 |
parent 71684 | 5036edb025b7 |
child 73340 | 0ffcad1f6130 |
permissions | -rw-r--r-- |
45674 | 1 |
/* Title: Pure/General/time.scala |
40393 | 2 |
Author: Makarius |
3 |
||
45674 | 4 |
Time based on milliseconds. |
40393 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
45664 | 9 |
|
50298 | 10 |
import java.util.Locale |
64056 | 11 |
import java.time.Instant |
50298 | 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) |
63700 | 17 |
def minutes(s: Double): Time = new Time((s * 60000.0).round) |
44699
5199ee17c7d7
property "tooltip-dismiss-delay" is edited in ms, not seconds;
wenzelm
parents:
40852
diff
changeset
|
18 |
def ms(m: Long): Time = new Time(m) |
63700 | 19 |
def hms(h: Int, m: Int, s: Double): Time = seconds(s + 60 * m + 3600 * h) |
63686 | 20 |
|
61528 | 21 |
def now(): Time = ms(System.currentTimeMillis()) |
22 |
||
51587 | 23 |
val zero: Time = ms(0) |
61528 | 24 |
val start: Time = now() |
51533 | 25 |
|
26 |
def print_seconds(s: Double): String = |
|
27 |
String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef]) |
|
64056 | 28 |
|
64058 | 29 |
def instant(t: Instant): Time = ms(t.getEpochSecond * 1000L + t.getNano / 1000000L) |
40393 | 30 |
} |
31 |
||
56351 | 32 |
final class Time private(val ms: Long) extends AnyVal |
40848
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40393
diff
changeset
|
33 |
{ |
65616 | 34 |
def proper_ms: Option[Long] = if (ms == 0) None else Some(ms) |
35 |
||
40848
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40393
diff
changeset
|
36 |
def seconds: Double = ms / 1000.0 |
63688
cc57255bf6ae
gnuplot presentation similar to former isatest-statistics;
wenzelm
parents:
63686
diff
changeset
|
37 |
def minutes: Double = ms / 60000.0 |
40852 | 38 |
|
56691 | 39 |
def + (t: Time): Time = new Time(ms + t.ms) |
40 |
def - (t: Time): Time = new Time(ms - t.ms) |
|
41 |
||
61602 | 42 |
def compare(t: Time): Int = ms compare t.ms |
56691 | 43 |
def < (t: Time): Boolean = ms < t.ms |
44 |
def <= (t: Time): Boolean = ms <= t.ms |
|
45 |
def > (t: Time): Boolean = ms > t.ms |
|
46 |
def >= (t: Time): Boolean = ms >= t.ms |
|
47 |
||
48 |
def min(t: Time): Time = if (this < t) this else t |
|
49 |
def max(t: Time): Time = if (this > t) this else t |
|
40852 | 50 |
|
53292
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
51587
diff
changeset
|
51 |
def is_zero: Boolean = ms == 0 |
46768 | 52 |
def is_relevant: Boolean = ms >= 1 |
53 |
||
57912 | 54 |
override def toString: String = Time.print_seconds(seconds) |
46768 | 55 |
|
40848
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40393
diff
changeset
|
56 |
def message: String = toString + "s" |
62571 | 57 |
|
58 |
def message_hms: String = |
|
59 |
{ |
|
60 |
val s = ms / 1000 |
|
61 |
String.format(Locale.ROOT, "%d:%02d:%02d", |
|
71163 | 62 |
java.lang.Long.valueOf(s / 3600), |
63 |
java.lang.Long.valueOf((s / 60) % 60), |
|
64 |
java.lang.Long.valueOf(s % 60)) |
|
62571 | 65 |
} |
64056 | 66 |
|
67 |
def instant: Instant = Instant.ofEpochMilli(ms) |
|
71684 | 68 |
|
69 |
def sleep { Thread.sleep(ms) } |
|
40848
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40393
diff
changeset
|
70 |
} |