tuned signature: more operations;

--- a/src/Pure/Admin/build_log.scala	Wed Jun 14 11:18:25 2023 +0200
+++ b/src/Pure/Admin/build_log.scala	Wed Jun 14 11:47:43 2023 +0200
@@ -686,7 +686,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 +
-          SQL.where(SQL.and(version1.defined, version2.defined)))
+          SQL.where_and(version1.defined, version2.defined))
     }
 
 
@@ -729,9 +729,9 @@
 
       SQL.Table("recent_pull_date", table.columns,
         table.select(table.columns, sql =
-          SQL.where(
-            SQL.or(pull_date(afp)(table).ident + " > " + recent_time(days),
-              SQL.and(eq_rev, eq_rev2)))))
+          SQL.where_or(
+            pull_date(afp)(table).ident + " > " + recent_time(days),
+            SQL.and(eq_rev, eq_rev2))))
     }
 
     def select_recent_log_names(days: Int): PostgreSQL.Source = {
@@ -1102,11 +1102,10 @@
         else (columns1, table1.ident)
 
       val where =
-        SQL.where(
-          SQL.and(
-            Data.log_name(table1).equal(log_name),
-            Data.session_name(table1).ident + " <> ''",
-            if_proper(session_names, Data.session_name(table1).member(session_names))))
+        SQL.where_and(
+          Data.log_name(table1).equal(log_name),
+          Data.session_name(table1).ident + " <> ''",
+          if_proper(session_names, Data.session_name(table1).member(session_names)))
 
       val sessions =
         db.execute_query_statement(

--- a/src/Pure/Admin/build_status.scala	Wed Jun 14 11:18:25 2023 +0200
+++ b/src/Pure/Admin/build_status.scala	Wed Jun 14 11:47:43 2023 +0200
@@ -61,15 +61,14 @@
         (if (ml_statistics) List(Build_Log.Data.ml_statistics) else Nil)
 
       Build_Log.Data.universal_table.select(columns, distinct = true, sql =
-        SQL.where(
-          SQL.and(
-            Build_Log.Data.pull_date(afp).ident + " > " + Build_Log.Data.recent_time(days(options)),
-            Build_Log.Data.status.member(
-              List(
-                Build_Log.Session_Status.finished.toString,
-                Build_Log.Session_Status.failed.toString)),
-            if_proper(only_sessions, Build_Log.Data.session_name.member(only_sessions)),
-            if_proper(sql, SQL.enclose(sql)))))
+        SQL.where_and(
+          Build_Log.Data.pull_date(afp).ident + " > " + Build_Log.Data.recent_time(days(options)),
+          Build_Log.Data.status.member(
+            List(
+              Build_Log.Session_Status.finished.toString,
+              Build_Log.Session_Status.failed.toString)),
+          if_proper(only_sessions, Build_Log.Data.session_name.member(only_sessions)),
+          if_proper(sql, SQL.enclose(sql))))
     }
   }
 

--- a/src/Pure/General/sql.scala	Wed Jun 14 11:18:25 2023 +0200
+++ b/src/Pure/General/sql.scala	Wed Jun 14 11:47:43 2023 +0200
@@ -81,6 +81,8 @@
     else OR(set.iterator.map(equal(sql, _)).toList)
 
   def where(sql: Source): Source = if_proper(sql, " WHERE " + sql)
+  def where_and(args: Source*): Source = where(and(args:_*))
+  def where_or(args: Source*): Source = where(or(args:_*))
 
 
   /* types */

--- a/src/Pure/Thy/document_build.scala	Wed Jun 14 11:18:25 2023 +0200
+++ b/src/Pure/Thy/document_build.scala	Wed Jun 14 11:47:43 2023 +0200
@@ -64,10 +64,9 @@
     val table = SQL.Table("isabelle_documents", List(session_name, name, sources, log_xz, pdf))
 
     def where_equal(session_name: String, name: String = ""): SQL.Source =
-      SQL.where(
-        SQL.and(
-          Data.session_name.equal(session_name),
-          if_proper(name, Data.name.equal(name))))
+      SQL.where_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	Wed Jun 14 11:18:25 2023 +0200
+++ b/src/Pure/Thy/export.scala	Wed Jun 14 11:47:43 2023 +0200
@@ -44,11 +44,10 @@
     val tables = SQL.Tables(table)
 
     def where_equal(session_name: String, theory_name: String = "", name: String = ""): SQL.Source =
-      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))))
+      SQL.where_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	Wed Jun 14 11:18:25 2023 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed Jun 14 11:47:43 2023 +0200
@@ -119,10 +119,9 @@
       SQL.Table("isabelle_sources", List(session_name, name, digest, compressed, body))
 
     def where_equal(session_name: String, name: String = ""): SQL.Source =
-      SQL.where(
-        SQL.and(
-          Sources.session_name.equal(session_name),
-          if_proper(name, Sources.name.equal(name))))
+      SQL.where_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(

--- a/src/Pure/Tools/build_process.scala	Wed Jun 14 11:18:25 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Wed Jun 14 11:47:43 2023 +0200
@@ -499,10 +499,9 @@
       db.execute_query_statement(
         Progress.table.select(
           sql =
-            SQL.where(
-              SQL.and(
-                if (seen <= 0) "" else Progress.serial.ident + " > " + seen,
-                Generic.sql(build_uuid = build_uuid)))),
+            SQL.where_and(
+              if (seen <= 0) "" else Progress.serial.ident + " > " + seen,
+              Generic.sql(build_uuid = build_uuid))),
         SortedMap.from[Long, isabelle.Progress.Message],
         { res =>
           val serial = res.long(Progress.serial)