src/Pure/General/time.scala
changeset 64056 0edc966bee55
parent 63700 2a95d904672e
child 64058 ea528dc9962d
--- 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)
 }