src/Pure/General/sql.scala

 Support for SQL databases: SQLite and PostgreSQL.
 */
 
 package isabelle
 
-
-import java.sql.{DriverManager, Connection, PreparedStatement, ResultSet, Timestamp}
+import java.time.OffsetDateTime
+import java.sql.{DriverManager, Connection, PreparedStatement, ResultSet}
 
 
 object SQL
 {
   /** SQL language **/

     def set_double(stmt: PreparedStatement, i: Int, x: Double) { stmt.setDouble(i, x) }
     def set_string(stmt: PreparedStatement, i: Int, x: String) { stmt.setString(i, x) }
     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 */
 
     def bool(rs: ResultSet, name: String): Boolean = rs.getBoolean(name)
     def int(rs: ResultSet, name: String): Int = rs.getInt(name)

     def bytes(rs: ResultSet, name: String): Bytes =
     {
       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] =
     {
       val x = f(rs, name)
       if (rs.wasNull) None else Some(x)

 
 /** SQLite **/
 
 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
     val s0 = File.platform_path(path0)
     val s1 = if (Platform.is_windows) s0.replace('\\', '/') else s0

   class Database private[SQLite](name: String, val connection: Connection) extends SQL.Database
   {
     override def toString: String = name
 
     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()) }
   }
 }
 

   {
     override def toString: String = name
 
     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) }
   }
 }