src/Pure/General/sql.scala

--- a/src/Pure/General/sql.scala	Fri Feb 10 10:34:14 2017 +0100
+++ b/src/Pure/General/sql.scala	Fri Feb 10 11:04:28 2017 +0100
@@ -6,8 +6,8 @@
 
 package isabelle
 
-
-import java.sql.{DriverManager, Connection, PreparedStatement, ResultSet, Timestamp}
+import java.time.OffsetDateTime
+import java.sql.{DriverManager, Connection, PreparedStatement, ResultSet}
 
 
 object SQL
@@ -207,8 +207,6 @@
     def set_bytes(stmt: PreparedStatement, i: Int, bytes: Bytes)
     { stmt.setBinaryStream(i, bytes.stream(), bytes.length) }
     def set_date(stmt: PreparedStatement, i: Int, date: Date)
-    { stmt.setTimestamp(i, date.timestamp) }
-
 
     /* output */
 
@@ -226,8 +224,7 @@
       val bs = rs.getBytes(name)
       if (bs == null) Bytes.empty else Bytes(bs)
     }
-    def date(rs: ResultSet, name: String): Date =
-      Date.instant(rs.getTimestamp(name).toInstant)
+    def date(rs: ResultSet, name: String): Date
 
     def get[A](rs: ResultSet, name: String, f: (ResultSet, String) => A): Option[A] =
     {
@@ -262,6 +259,9 @@
 
 object SQLite
 {
+  // see https://www.sqlite.org/lang_datefunc.html
+  val date_format: Date.Format = Date.Format("uuuu-MM-dd HH:mm:ss.SSS x")
+
   def open_database(path: Path): Database =
   {
     val path0 = path.expand
@@ -277,6 +277,11 @@
 
     def sql_type(T: SQL.Type.Value): String = SQL.sql_type_sqlite(T)
 
+    def set_date(stmt: PreparedStatement, i: Int, date: Date): Unit =
+      set_string(stmt, i, date_format(date))
+    def date(rs: ResultSet, name: String): Date =
+      date_format.parse(string(rs, name))
+
     def rebuild { using(statement("VACUUM"))(_.execute()) }
   }
 }
@@ -331,6 +336,12 @@
 
     def sql_type(T: SQL.Type.Value): String = SQL.sql_type_postgresql(T)
 
+    // see https://jdbc.postgresql.org/documentation/head/8-date-time.html
+    def set_date(stmt: PreparedStatement, i: Int, date: Date): Unit =
+      stmt.setObject(i, OffsetDateTime.from(date.to_utc.rep))
+    def date(rs: ResultSet, name: String): Date =
+      Date.instant(rs.getObject(name, classOf[OffsetDateTime]).toInstant)
+
     override def close() { super.close; port_forwarding.foreach(_.close) }
   }
 }