support for type Date;

--- a/src/Pure/General/date.scala	Thu Feb 09 20:47:41 2017 +0100
+++ b/src/Pure/General/date.scala	Thu Feb 09 22:40:15 2017 +0100
@@ -8,7 +8,8 @@
 
 
 import java.util.Locale
-import java.time.{Instant, ZonedDateTime, LocalTime, ZoneId}
+import java.sql.Timestamp
+import java.time.{Instant, ZonedDateTime, LocalTime, ZoneId, OffsetDateTime}
 import java.time.format.{DateTimeFormatter, DateTimeParseException}
 import java.time.temporal.TemporalAccessor
 
@@ -79,8 +80,10 @@
 
   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))
+  def instant(t: Instant, zone: ZoneId = timezone()): Date =
+    new Date(ZonedDateTime.ofInstant(t, zone))
+
+  def apply(t: Time, zone: ZoneId = timezone()): Date = instant(t.instant, zone)
 }
 
 sealed case class Date(rep: ZonedDateTime)
@@ -91,7 +94,9 @@
   def to(zone: ZoneId): Date = new Date(rep.withZoneSameInstant(zone))
   def to_utc: Date = to(ZoneId.of("UTC"))
 
-  def time: Time = Time.instant(Instant.from(rep))
+  def instant: Instant = Instant.from(rep)
+  def timestamp: Timestamp = Timestamp.from(instant)
+  def time: Time = Time.instant(instant)
   def timezone: ZoneId = rep.getZone
 
   def format(fmt: Date.Format = Date.Format.default): String = fmt(this)

--- a/src/Pure/General/sql.scala	Thu Feb 09 20:47:41 2017 +0100
+++ b/src/Pure/General/sql.scala	Thu Feb 09 22:40:15 2017 +0100
@@ -7,7 +7,7 @@
 package isabelle
 
 
-import java.sql.{DriverManager, Connection, PreparedStatement, ResultSet}
+import java.sql.{DriverManager, Connection, PreparedStatement, ResultSet, Timestamp}
 
 
 object SQL
@@ -49,6 +49,7 @@
     val Double = Value("DOUBLE PRECISION")
     val String = Value("TEXT")
     val Bytes = Value("BLOB")
+    val Date = Value("TIMESTAMP WITH TIME ZONE")
   }
 
   type Type_Name = Type.Value => String
@@ -57,6 +58,7 @@
 
   def type_name_sqlite(t: Type.Value): String =
     if (t == Type.Boolean) "INTEGER"
+    else if (t == Type.Date) "TEXT"
     else type_name_default(t)
 
   def type_name_postgresql(t: Type.Value): String =
@@ -80,6 +82,8 @@
       new Column_String(name, strict, primary_key)
     def bytes(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[Bytes] =
       new Column_Bytes(name, strict, primary_key)
+    def date(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[Date] =
+      new Column_Date(name, strict, primary_key)
   }
 
   abstract class Column[+A] private[SQL](
@@ -153,6 +157,15 @@
     }
   }
 
+  class Column_Date private[SQL](name: String, strict: Boolean, primary_key: Boolean)
+    extends Column[Date](name, strict, primary_key, Type.Date)
+  {
+    def apply(rs: ResultSet): Date =
+    {
+      Date.instant(rs.getTimestamp(name).toInstant)
+    }
+  }
+
 
   /* tables */