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) } } }