# HG changeset patch
# User wenzelm
# Date 1678362859 -3600
# Node ID 6370d9e5ab50efdd91323875ff56d474feee550d
# Parent  308f3f48c2c70afcc9a223634d9704c7f2fd019d
proper support for Option[Date] columns;

diff -r 308f3f48c2c7 -r 6370d9e5ab50 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Thu Mar 09 12:13:01 2023 +0100
+++ b/src/Pure/General/sql.scala	Thu Mar 09 12:54:19 2023 +0100
@@ -330,7 +330,7 @@
 
     def get[A](column: Column, f: Column => A): Option[A] = {
       val x = f(column)
-      if (rep.wasNull) None else Some(x)
+      if (rep.wasNull || x == null) None else Some(x)
     }
     def get_bool(column: Column): Option[Boolean] = get(column, bool)
     def get_int(column: Column): Option[Int] = get(column, int)
@@ -494,7 +494,10 @@
       else stmt.string(i) = date_format(date)
 
     def date(res: SQL.Result, column: SQL.Column): Date =
-      date_format.parse(res.string(column))
+      proper_string(res.string(column)) match {
+        case None => null
+        case Some(s) => date_format.parse(s)
+      }
 
     def insert_permissive(table: SQL.Table, sql: SQL.Source = ""): SQL.Source =
       table.insert_cmd(cmd = "INSERT OR IGNORE", sql = sql)