# HG changeset patch
# User wenzelm
# Date 1486721068 -3600
# Node ID da8ae577d171d22df8648aba88a269019b02bbbb
# Parent  a4fcaeadc825dd2714dc6f01a143ce1050eb54e2
clarified Date storage;

diff -r a4fcaeadc825 -r da8ae577d171 src/Pure/General/date.scala
--- a/src/Pure/General/date.scala	Fri Feb 10 10:34:14 2017 +0100
+++ b/src/Pure/General/date.scala	Fri Feb 10 11:04:28 2017 +0100
@@ -8,7 +8,6 @@
 
 
 import java.util.Locale
-import java.sql.Timestamp
 import java.time.{Instant, ZonedDateTime, LocalTime, ZoneId, OffsetDateTime}
 import java.time.format.{DateTimeFormatter, DateTimeParseException}
 import java.time.temporal.TemporalAccessor
@@ -39,7 +38,6 @@
     val default: Format = Format("dd-MMM-uuuu HH:mm:ss xx")
     val date: Format = Format("dd-MMM-uuuu")
     val time: Format = Format("HH:mm:ss")
-    val timestamp: Format = Format("uuuu-MM-dd HH:mm:ss.SSS x")
   }
 
   abstract class Format private
@@ -96,7 +94,6 @@
   def to_utc: Date = to(ZoneId.of("UTC"))
 
   def instant: Instant = Instant.from(rep)
-  def timestamp: Timestamp = Timestamp.from(instant)
   def time: Time = Time.instant(instant)
   def timezone: ZoneId = rep.getZone
 
diff -r a4fcaeadc825 -r da8ae577d171 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) }
   }
 }