# HG changeset patch
# User wenzelm
# Date 1507922104 -7200
# Node ID 6b90c688a6dc089de7bdc8f02d9b9c0b0c6f2303
# Parent  c9d413fca1ece26f92302df4773a6b00e75794f2
tuned signature;

diff -r c9d413fca1ec -r 6b90c688a6dc src/Pure/Admin/build_log.scala
--- 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) +
diff -r c9d413fca1ec -r 6b90c688a6dc src/Pure/Admin/isabelle_cronjob.scala
--- 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")),
diff -r c9d413fca1ec -r 6b90c688a6dc src/Pure/General/sql.scala
--- 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