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 java.lang.Long.valueOf(s / 3600), 63 java.lang.Long.valueOf((s / 60) % 60), 64 java.lang.Long.valueOf(s % 60)) 65 } 66 67 def instant: Instant = Instant.ofEpochMilli(ms) 68} 69