# HG changeset patch
# User wenzelm
# Date 1709999454 -3600
# Node ID 2a3c0a68221cc7a3e761b0196a5be80e38b043f0
# Parent  4611b7b47b4237e5c7976d39fe8c31b06b8636ed
misc tuning: prefer Build_Process.Update operations;

diff -r 4611b7b47b42 -r 2a3c0a68221c src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Sat Mar 09 16:45:18 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Sat Mar 09 16:50:54 2024 +0100
@@ -1081,10 +1081,10 @@
           SQL.where(if_proper(build_uuid, Schedules.build_uuid.equal(build_uuid)))),
           _.long(Schedules.serial)).getOrElse(0L)
 
-    def read_scheduled_builds_domain(db: SQL.Database): List[String] =
+    def read_scheduled_builds_domain(db: SQL.Database): Map[String, Unit] =
       db.execute_query_statement(
         Schedules.table.select(List(Schedules.build_uuid)),
-        List.from[String], res => res.string(Schedules.build_uuid))
+        Map.from[String, Unit], res => res.string(Schedules.build_uuid) -> ())
 
     def read_schedules(db: SQL.Database, build_uuid: String = ""): List[Schedule] = {
       val schedules =
@@ -1207,12 +1207,12 @@
       val running_builds_domain =
         db.execute_query_statement(
           Base.table.select(List(Base.build_uuid), sql = SQL.where(Base.stop.undefined)),
-          List.from[String], res => res.string(Base.build_uuid))
+          Map.from[String, Unit], res => res.string(Base.build_uuid) -> ())
 
-      val (remove, _) =
-        Library.symmetric_difference(read_scheduled_builds_domain(db), running_builds_domain)
+      val update =
+        Build_Process.data_update(read_scheduled_builds_domain(db), running_builds_domain)
 
-      remove_schedules(db, remove)
+      remove_schedules(db, update.delete)
     }
 
     override val tables: SQL.Tables = SQL.Tables(Schedules.table, Nodes.table)