--- a/src/Pure/Admin/build_log.scala Fri Oct 13 21:09:35 2017 +0200
+++ b/src/Pure/Admin/build_log.scala Fri Oct 13 21:15:04 2017 +0200
@@ -692,7 +692,7 @@
val version2 = Prop.afp_version
build_log_table("isabelle_afp_versions", List(version1.copy(primary_key = true), version2),
SQL.select(List(version1, version2), distinct = true) + meta_info_table +
- " WHERE " + version1 + " IS NOT NULL AND " + version2 + " IS NOT NULL")
+ " WHERE " + version1.defined + " AND " + version2.defined)
}
@@ -706,7 +706,7 @@
build_log_table("pull_date", List(version.copy(primary_key = true), pull_date),
"SELECT " + version + ", min(" + Prop.build_start + ") AS " + pull_date +
" FROM " + meta_info_table +
- " WHERE " + version + " IS NOT NULL AND " + Prop.build_start + " IS NOT NULL" +
+ " WHERE " + version.defined + " AND " + Prop.build_start.defined +
" GROUP BY " + version)
}
@@ -753,7 +753,7 @@
val columns =
List(Prop.isabelle_version(table1), pull_date(table1),
- known.copy(expr = log_name(aux_table) + " IS NOT NULL"))
+ known.copy(expr = log_name(aux_table).defined))
SQL.select(columns, distinct = true) +
table1.query_named + SQL.join_outer + aux_table.query_named +
" ON " + Prop.isabelle_version(table1) + " = " + Prop.isabelle_version(aux_table) +
--- a/src/Pure/Admin/isabelle_cronjob.scala Fri Oct 13 21:09:35 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Fri Oct 13 21:15:04 2017 +0200
@@ -197,7 +197,7 @@
" -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" +
" -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_SMLNJ=/mnt/nfsbroy/home/smlnj/bin/sml",
args = "-a",
- detect = Build_Log.Prop.build_tags + " IS NULL"),
+ detect = Build_Log.Prop.build_tags.undefined),
Remote_Build("Mac OS X 10.9 Mavericks, quick_and_dirty", "macbroy2",
options = "-m32 -M8 -t quick_and_dirty", args = "-a -o quick_and_dirty",
detect = Build_Log.Prop.build_tags + " = " + SQL.string("quick_and_dirty")),
--- a/src/Pure/General/sql.scala Fri Oct 13 21:09:35 2017 +0200
+++ b/src/Pure/General/sql.scala Fri Oct 13 21:15:04 2017 +0200
@@ -115,6 +115,9 @@
def decl(sql_type: Type.Value => Source): Source =
ident + " " + sql_type(T) + (if (strict || primary_key) " NOT NULL" else "")
+ def defined: String = ident + " IS NOT NULL"
+ def undefined: String = ident + " IS NULL"
+
def where_equal(s: String): Source = "WHERE " + ident + " = " + string(s)
override def toString: Source = ident