# HG changeset patch
# User wenzelm
# Date 1677415807 -3600
# Node ID 324f5821a4a4d597c2f6646d896458a58bed64bf
# Parent  268bf61631ec23b8a2f51cdadcf90a559614a78f
clarified signature: more concise operations;

diff -r 268bf61631ec -r 324f5821a4a4 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Sun Feb 26 13:15:41 2023 +0100
+++ b/src/Pure/Admin/build_log.scala	Sun Feb 26 13:50:07 2023 +0100
@@ -1068,7 +1068,7 @@
         Data.session_name(table1) + " <> ''"
       val where =
         if (session_names.isEmpty) where_log_name
-        else where_log_name + " AND " + SQL.member(Data.session_name(table1).ident, session_names)
+        else where_log_name + " AND " + Data.session_name(table1).member(session_names)
 
       val columns1 = table1.columns.tail.map(_.apply(table1))
       val (columns, from) =
diff -r 268bf61631ec -r 324f5821a4a4 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Sun Feb 26 13:15:41 2023 +0100
+++ b/src/Pure/Admin/build_status.scala	Sun Feb 26 13:50:07 2023 +0100
@@ -40,12 +40,11 @@
         sql = "WHERE " +
           Build_Log.Data.pull_date(afp) + " > " + Build_Log.Data.recent_time(days(options)) +
           " AND " +
-          SQL.member(Build_Log.Data.status.ident,
+          Build_Log.Data.status.member(
             List(
               Build_Log.Session_Status.finished.toString,
               Build_Log.Session_Status.failed.toString)) +
-          if_proper(only_sessions,
-            " AND " + SQL.member(Build_Log.Data.session_name.ident, only_sessions)) +
+          if_proper(only_sessions, " AND " + Build_Log.Data.session_name.member(only_sessions)) +
           " AND " + SQL.enclose(sql))
     }
   }
diff -r 268bf61631ec -r 324f5821a4a4 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sun Feb 26 13:15:41 2023 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sun Feb 26 13:50:07 2023 +0100
@@ -156,8 +156,8 @@
 
     def sql: PostgreSQL.Source =
       SQL.and(
-        Build_Log.Prop.build_engine.toString + " = " + SQL.string(Build_History.engine),
-        SQL.member(Build_Log.Prop.build_host.ident, host :: more_hosts),
+        Build_Log.Prop.build_engine.equal(Build_History.engine),
+        Build_Log.Prop.build_host.member(host :: more_hosts),
         if_proper(detect, SQL.enclose(detect)))
 
     def profile: Build_Status.Profile =
diff -r 268bf61631ec -r 324f5821a4a4 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sun Feb 26 13:15:41 2023 +0100
+++ b/src/Pure/General/sql.scala	Sun Feb 26 13:50:07 2023 +0100
@@ -69,16 +69,15 @@
   val TRUE: Source = "TRUE"
   val FALSE: Source = "FALSE"
 
-  def member(x: Source, set: Iterable[String]): Source =
+  def equal(sql: Source, s: String): Source = sql + " = " + string(s)
+
+  def member(sql: Source, set: Iterable[String]): Source =
     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)
+    else OR(set.iterator.map(equal(sql, _)).toList)
 
   def where(sql: Source): Source = if_proper(sql, " WHERE " + sql)
 
 
-
   /* types */
 
   object Type extends Enumeration {
@@ -144,8 +143,11 @@
     def defined: String = ident + " IS NOT NULL"
     def undefined: String = ident + " IS NULL"
 
-    def equal(s: String): Source = ident + " = " + string(s)
-    def where_equal(s: String): Source = " WHERE " + equal(s)
+    def equal(s: String): Source = SQL.equal(ident, s)
+    def member(set: Iterable[String]): Source = SQL.member(ident, set)
+
+    def where_equal(s: String): Source = SQL.where(equal(s))
+    def where_member(set: Iterable[String]): Source = SQL.where(member(set))
 
     override def toString: Source = ident
   }
diff -r 268bf61631ec -r 324f5821a4a4 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sun Feb 26 13:15:41 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Sun Feb 26 13:50:07 2023 +0100
@@ -246,7 +246,7 @@
       def sql_member(instance: String = "", names: Iterable[String] = Nil): SQL.Source =
         SQL.and(
           if_proper(instance, Generic.instance.equal(instance)),
-          if_proper(names, SQL.member(Generic.name.toString, names)))
+          if_proper(names, Generic.name.member(names)))
     }
 
     object Config {
@@ -367,7 +367,7 @@
 
     def read_results(db: SQL.Database, names: List[String] = Nil): Map[String, Build_Job.Result] =
       db.using_statement(
-        Results.table.select() + if_proper(names, SQL.where_member(Results.name.toString, names))
+        Results.table.select() + if_proper(names, Results.name.where_member(names))
       ) { stmt =>
         Map.from(
           stmt.execute_query().iterator { res =>