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