clarified signature: more robust operations;

--- a/src/Pure/Admin/build_log.scala	Fri Feb 24 20:52:35 2023 +0100
+++ b/src/Pure/Admin/build_log.scala	Sat Feb 25 14:33:19 2023 +0100
@@ -681,7 +681,7 @@
       val version2 = Prop.afp_version
       build_log_table("isabelle_afp_versions", List(version1.make_primary_key, version2),
         SQL.select(List(version1, version2), distinct = true) + meta_info_table +
-        " WHERE " + version1.defined + " AND " + version2.defined)
+          SQL.where(SQL.and(version1.defined, version2.defined)))
     }
 
 
@@ -700,7 +700,7 @@
         "SELECT " + versions.mkString(", ") +
           ", min(" + Prop.build_start + ") AS " + pull_date(afp) +
         " FROM " + meta_info_table +
-        " WHERE " + (versions ::: List(Prop.build_start)).map(_.defined).mkString(" AND ") +
+        " WHERE " + SQL.AND((versions ::: List(Prop.build_start)).map(_.defined)) +
         " GROUP BY " + versions.mkString(", "))
     }
 

--- a/src/Pure/Admin/isabelle_cronjob.scala	Fri Feb 24 20:52:35 2023 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sat Feb 25 14:33:19 2023 +0100
@@ -155,9 +155,10 @@
       SSH.open_session(options, host = host, user = user, port = port)
 
     def sql: PostgreSQL.Source =
-      Build_Log.Prop.build_engine.toString + " = " + SQL.string(Build_History.engine) + " AND " +
-      SQL.member(Build_Log.Prop.build_host.ident, host :: more_hosts) +
-      if_proper(detect, " AND " + SQL.enclose(detect))
+      SQL.and(
+        Build_Log.Prop.build_engine.toString + " = " + SQL.string(Build_History.engine),
+        SQL.member(Build_Log.Prop.build_host.ident, host :: more_hosts),
+        if_proper(detect, SQL.enclose(detect)))
 
     def profile: Build_Status.Profile =
       Build_Status.Profile(description, history = history, afp = afp, bulky = bulky, sql = sql)

--- a/src/Pure/General/sql.scala	Fri Feb 24 20:52:35 2023 +0100
+++ b/src/Pure/General/sql.scala	Sat Feb 25 14:33:19 2023 +0100
@@ -55,12 +55,29 @@
   val join_inner: Source = " INNER JOIN "
   def join(outer: Boolean): Source = if (outer) join_outer else join_inner
 
+  def infix(op: Source, args: Iterable[Source]): Source = {
+    val body = args.iterator.filter(_.nonEmpty).mkString(" " + op + " ")
+    if_proper(body, enclose(body))
+  }
+
+  def AND(args: Iterable[Source]): Source = infix("AND", args)
+  def OR(args: Iterable[Source]): Source = infix("OR", args)
+
+  def and(args: Source*): Source = AND(args)
+  def or(args: Source*): Source = OR(args)
+
+  val TRUE: Source = "TRUE"
+  val FALSE: Source = "FALSE"
+
   def member(x: Source, set: Iterable[String]): Source =
-    if (set.isEmpty) "FALSE"
-    else set.iterator.map(a => x + " = " + SQL.string(a)).mkString("(", " OR ", ")")
+    if (set.isEmpty) FALSE
+    else OR(set.iterator.map(a => x + " = " + SQL.string(a)).toList)
 
   def where_member(x: Source, set: Iterable[String]): Source = " WHERE " + member(x, set)
 
+  def where(sql: Source): Source = if_proper(sql, " WHERE " + sql)
+
+
 
   /* types */
 
@@ -128,7 +145,7 @@
     def undefined: String = ident + " IS NULL"
 
     def equal(s: String): Source = ident + " = " + string(s)
-    def where_equal(s: String): Source = "WHERE " + equal(s)
+    def where_equal(s: String): Source = " WHERE " + equal(s)
 
     override def toString: Source = ident
   }

--- a/src/Pure/Thy/document_build.scala	Fri Feb 24 20:52:35 2023 +0100
+++ b/src/Pure/Thy/document_build.scala	Sat Feb 25 14:33:19 2023 +0100
@@ -64,8 +64,10 @@
     val table = SQL.Table("isabelle_documents", List(session_name, name, sources, log_xz, pdf))
 
     def where_equal(session_name: String, name: String = ""): SQL.Source =
-      "WHERE " + Data.session_name.equal(session_name) +
-        (if (name == "") "" else " AND " + Data.name.equal(name))
+      SQL.where(
+        SQL.and(
+          Data.session_name.equal(session_name),
+          if_proper(name, Data.name.equal(name))))
   }
 
   def read_documents(db: SQL.Database, session_name: String): List[Document_Input] = {

--- a/src/Pure/Thy/export.scala	Fri Feb 24 20:52:35 2023 +0100
+++ b/src/Pure/Thy/export.scala	Sat Feb 25 14:33:19 2023 +0100
@@ -42,9 +42,11 @@
         List(session_name, theory_name, name, executable, compressed, body))
 
     def where_equal(session_name: String, theory_name: String = "", name: String = ""): SQL.Source =
-      "WHERE " + Data.session_name.equal(session_name) +
-        (if (theory_name == "") "" else " AND " + Data.theory_name.equal(theory_name)) +
-        (if (name == "") "" else " AND " + Data.name.equal(name))
+      SQL.where(
+        SQL.and(
+          Data.session_name.equal(session_name),
+          if_proper(theory_name, Data.theory_name.equal(theory_name)),
+          if_proper(name, Data.name.equal(name))))
   }
 
   def compound_name(a: String, b: String): String =

--- a/src/Pure/Thy/sessions.scala	Fri Feb 24 20:52:35 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Sat Feb 25 14:33:19 2023 +0100
@@ -77,8 +77,10 @@
       SQL.Table("isabelle_sources", List(session_name, name, digest, compressed, body))
 
     def where_equal(session_name: String, name: String = ""): SQL.Source =
-      "WHERE " + Sources.session_name.equal(session_name) +
-        (if (name == "") "" else " AND " + Sources.name.equal(name))
+      SQL.where(
+        SQL.and(
+          Sources.session_name.equal(session_name),
+          if_proper(name, Sources.name.equal(name))))
 
     def load(session_base: Base, cache: Compress.Cache = Compress.Cache.none): Sources =
       new Sources(