# HG changeset patch
# User wenzelm
# Date 1475689536 -7200
# Node ID 0edc966bee552c288bd57642f77c4483166f9e8d
# Parent  acd3e25975a2ebd326f5509b1b272c3cb3e1f637
more date and time operations from Java 8;

diff -r acd3e25975a2 -r 0edc966bee55 src/Pure/Concurrent/event_timer.scala
--- a/src/Pure/Concurrent/event_timer.scala	Wed Oct 05 14:34:42 2016 +0200
+++ b/src/Pure/Concurrent/event_timer.scala	Wed Oct 05 19:45:36 2016 +0200
@@ -11,7 +11,7 @@
 package isabelle
 
 
-import java.util.{Timer, TimerTask, Date}
+import java.util.{Timer, TimerTask, Date => JDate}
 
 
 object Event_Timer
@@ -26,7 +26,7 @@
   def request(time: Time)(event: => Unit): Request =
   {
     val task = new TimerTask { def run { event } }
-    event_timer.schedule(task, new Date(time.ms))
+    event_timer.schedule(task, new JDate(time.ms))
     new Request(time, task)
   }
 }
diff -r acd3e25975a2 -r 0edc966bee55 src/Pure/General/date.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/date.scala	Wed Oct 05 19:45:36 2016 +0200
@@ -0,0 +1,55 @@
+/*  Title:      Pure/General/date.scala
+    Author:     Makarius
+
+Date and time, with time zone.
+*/
+
+package isabelle
+
+
+import java.time.{ZonedDateTime, ZoneId}
+import java.time.format.{DateTimeFormatter, DateTimeParseException}
+
+
+object Date
+{
+  def timezone(): ZoneId = ZoneId.systemDefault
+
+  def now(zone: ZoneId = timezone()): Date = new Date(ZonedDateTime.now(zone))
+
+  def apply(t: Time, zone: ZoneId = timezone()): Date =
+    new Date(ZonedDateTime.ofInstant(t.instant, zone))
+
+
+  /* format */
+
+  object Format
+  {
+    def apply(fmt: DateTimeFormatter): Format =
+      new Format {
+        def apply(date: Date): String = fmt.format(date.rep)
+        def parse(str: String): Date = new Date(ZonedDateTime.from(fmt.parse(str)))
+      }
+
+    def apply(pattern: String): Format =
+      apply(DateTimeFormatter.ofPattern(pattern))
+
+    val default: Format = apply("dd-MMM-uuuu HH:mm:ss xx")
+    val default_date: Format = apply("dd-MMM-uuuu")
+    val default_time: Format = apply("HH:mm:ss")
+  }
+
+  abstract class Format private
+  {
+    def apply(date: Date): String
+    def parse(str: String): Date
+    def unapply(str: String): Option[Date] =
+      try { Some(parse(str)) }
+      catch { case _: DateTimeParseException => None }
+  }
+}
+
+sealed case class Date private(private[Date] rep: ZonedDateTime)
+{
+  override def toString: String = Date.Format.default(this)
+}
diff -r acd3e25975a2 -r 0edc966bee55 src/Pure/General/time.scala
--- 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)
 }
diff -r acd3e25975a2 -r 0edc966bee55 src/Pure/build-jars
--- a/src/Pure/build-jars	Wed Oct 05 14:34:42 2016 +0200
+++ b/src/Pure/build-jars	Wed Oct 05 19:45:36 2016 +0200
@@ -27,6 +27,7 @@
   General/antiquote.scala
   General/bytes.scala
   General/completion.scala
+  General/date.scala
   General/exn.scala
   General/file.scala
   General/graph.scala