--- a/src/Pure/General/time.scala Wed Oct 05 14:34:42 2016 +0200
+++ b/src/Pure/General/time.scala Wed Oct 05 19:45:36 2016 +0200
@@ -9,6 +9,7 @@
import java.util.Locale
+import java.time.Instant
object Time
@@ -25,6 +26,8 @@
def print_seconds(s: Double): String =
String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])
+
+ def instant(t: Instant): Time = ms(t.getEpochSecond + t.getNano / 1000000L)
}
final class Time private(val ms: Long) extends AnyVal
@@ -57,4 +60,6 @@
String.format(Locale.ROOT, "%d:%02d:%02d",
new java.lang.Long(s / 3600), new java.lang.Long((s / 60) % 60), new java.lang.Long(s % 60))
}
+
+ def instant: Instant = Instant.ofEpochMilli(ms)
}