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