src/Pure/General/sql.scala

--- 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 */