# HG changeset patch
# User wenzelm
# Date 1678820688 -3600
# Node ID b45fc98d11ea8c184e377fc13d221c93d4c942fd
# Parent  45bd5c26cbcc3e930998137ec1f646a9dfa12729
tuned signature;

diff -r 45bd5c26cbcc -r b45fc98d11ea src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Tue Mar 14 20:01:05 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Tue Mar 14 20:04:48 2023 +0100
@@ -342,6 +342,16 @@
           if_proper(worker_uuid, Generic.worker_uuid.equal(worker_uuid)),
           if_proper(name, Generic.name.equal(name)),
           if_proper(names, Generic.name.member(names)))
+
+      def sql_where(
+        build_uuid: String = "",
+        worker_uuid: String = "",
+        name: String = "",
+        names: Iterable[String] = Nil
+      ): SQL.Source = {
+        SQL.where(sql(build_uuid = build_uuid, worker_uuid = worker_uuid,
+          name = name, names = names))
+      }
     }
 
 
@@ -361,7 +371,7 @@
 
     def read_builds(db: SQL.Database, build_uuid: String = ""): List[Build] =
       db.execute_query_statement(
-        Base.table.select(sql = SQL.where(Generic.sql(build_uuid = build_uuid))),
+        Base.table.select(sql = Generic.sql_where(build_uuid = build_uuid)),
         List.from[Build],
         { res =>
           val build_uuid = res.string(Base.build_uuid)
@@ -582,8 +592,8 @@
       worker_uuid: String = ""
     ): List[Worker] = {
       db.execute_query_statement(
-        Workers.table.select(sql =
-          SQL.where(Generic.sql(build_uuid = build_uuid, worker_uuid = worker_uuid))),
+        Workers.table.select(
+          sql = Generic.sql_where(build_uuid = build_uuid, worker_uuid = worker_uuid)),
           List.from[Worker],
           { res =>
             Worker(
@@ -685,7 +695,7 @@
 
       if (delete.nonEmpty) {
         db.execute_statement(
-          Pending.table.delete(sql = SQL.where(Generic.sql(names = delete.map(_.name)))))
+          Pending.table.delete(sql = Generic.sql_where(names = delete.map(_.name))))
       }
 
       for (task <- insert) {
@@ -736,7 +746,7 @@
 
       if (delete.nonEmpty) {
         db.execute_statement(
-          Running.table.delete(sql = SQL.where(Generic.sql(names = delete.map(_.name)))))
+          Running.table.delete(sql = Generic.sql_where(names = delete.map(_.name))))
       }
 
       for (job <- insert) {