1/*  Title:      Pure/General/time.scala
2    Author:     Makarius
3
4Time based on milliseconds.
5*/
6
7package isabelle
8
9
10import java.util.Locale
11import java.time.Instant
12
13
14object Time
15{
16  def seconds(s: Double): Time = new Time((s * 1000.0).round)
17  def minutes(s: Double): Time = new Time((s * 60000.0).round)
18  def ms(m: Long): Time = new Time(m)
19  def hms(h: Int, m: Int, s: Double): Time = seconds(s + 60 * m + 3600 * h)
20
21  def now(): Time = ms(System.currentTimeMillis())
22
23  val zero: Time = ms(0)
24  val start: Time = now()
25
26  def print_seconds(s: Double): String =
27    String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])
28
29  def instant(t: Instant): Time = ms(t.getEpochSecond * 1000L + t.getNano / 1000000L)
30}
31
32final class Time private(val ms: Long) extends AnyVal
33{
34  def proper_ms: Option[Long] = if (ms == 0) None else Some(ms)
35
36  def seconds: Double = ms / 1000.0
37  def minutes: Double = ms / 60000.0
38
39  def + (t: Time): Time = new Time(ms + t.ms)
40  def - (t: Time): Time = new Time(ms - t.ms)
41
42  def compare(t: Time): Int = ms compare t.ms
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
50
51  def is_zero: Boolean = ms == 0
52  def is_relevant: Boolean = ms >= 1
53
54  override def toString: String = Time.print_seconds(seconds)
55
56  def message: String = toString + "s"
57
58  def message_hms: String =
59  {
60    val s = ms / 1000
61    String.format(Locale.ROOT, "%d:%02d:%02d",
62      new java.lang.Long(s / 3600), new java.lang.Long((s / 60) % 60), new java.lang.Long(s % 60))
63  }
64
65  def instant: Instant = Instant.ofEpochMilli(ms)
66}
67