# HG changeset patch
# User wenzelm
# Date 1709999978 -3600
# Node ID 45b81ff3c97244e15dea949d7dbc86fd2f1f43d2
# Parent  d71af537a6e960895b4668eb60c1a7570a87fa30
clarified modules;

diff -r d71af537a6e9 -r 45b81ff3c972 src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Sat Mar 09 16:52:08 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Sat Mar 09 16:59:38 2024 +0100
@@ -16,28 +16,6 @@
 object Build_Process {
   /** state vs. database **/
 
-  object Update {
-    val empty: Update = Update()
-  }
-  sealed case class Update(
-    domain: Set[String] = Set.empty,
-    delete: List[String] = Nil,
-    insert: List[String] = Nil
-  ) {
-    def deletes: Boolean = delete.nonEmpty
-    def inserts: Boolean = insert.nonEmpty
-    def defined: Boolean = deletes || inserts
-  }
-
-  def data_update[A](data0: Map[String, A], data1: Map[String, A]): Update =
-    if (data0.eq(data1)) Update.empty
-    else {
-      val delete = List.from(for ((x, y) <- data0.iterator if !data1.get(x).contains(y)) yield x)
-      val insert = List.from(for ((x, y) <- data1.iterator if !data0.get(x).contains(y)) yield x)
-      val domain = delete.toSet ++ insert
-      Update(domain = domain, delete = delete, insert = insert)
-    }
-
   sealed case class Build(
     build_uuid: String,   // Database_Progress.context_uuid
     ml_platform: String,
@@ -109,9 +87,9 @@
     type Graph = isabelle.Graph[String, Build_Job.Session_Context]
     val empty: Sessions = new Sessions(Graph.string)
 
-    def update(sessions0: Sessions, sessions1: Sessions): Update =
-      if (sessions0.eq(sessions1)) Update.empty
-      else data_update(sessions0.data, sessions1.data)
+    def update(sessions0: Sessions, sessions1: Sessions): Library.Update =
+      if (sessions0.eq(sessions1)) Library.Update.empty
+      else Library.Update.make(sessions0.data, sessions1.data)
   }
 
   final class Sessions private(val graph: Sessions.Graph) {
@@ -635,7 +613,7 @@
       pending: State.Pending,
       old_pending: State.Pending
     ): Boolean = {
-      val update = data_update(old_pending, pending)
+      val update = Library.Update.make(old_pending, pending)
 
       if (update.deletes) {
         db.execute_statement(
@@ -696,7 +674,7 @@
       running: State.Running,
       old_running: State.Running
     ): Boolean = {
-      val update = data_update(old_running, running)
+      val update = Library.Update.make(old_running, running)
 
       if (update.deletes) {
         db.execute_statement(
@@ -791,7 +769,7 @@
       results: State.Results,
       old_results: State.Results
     ): Boolean = {
-      val update = data_update(old_results, results)
+      val update = Library.Update.make(old_results, results)
 
       if (update.deletes) {
         db.execute_statement(
diff -r d71af537a6e9 -r 45b81ff3c972 src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Sat Mar 09 16:52:08 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Sat Mar 09 16:59:38 2024 +0100
@@ -1209,8 +1209,7 @@
           Base.table.select(List(Base.build_uuid), sql = SQL.where(Base.stop.undefined)),
           Map.from[String, Unit], res => res.string(Base.build_uuid) -> ())
 
-      val update =
-        Build_Process.data_update(read_scheduled_builds_domain(db), running_builds_domain)
+      val update = Library.Update.make(read_scheduled_builds_domain(db), running_builds_domain)
 
       remove_schedules(db, update.delete)
     }
diff -r d71af537a6e9 -r 45b81ff3c972 src/Pure/library.scala
--- a/src/Pure/library.scala	Sat Mar 09 16:52:08 2024 +0100
+++ b/src/Pure/library.scala	Sat Mar 09 16:59:38 2024 +0100
@@ -285,6 +285,34 @@
     }
 
 
+  /* data update */
+
+  object Update {
+    type Data[A] = Map[String, A]
+
+    val empty: Update = Update()
+
+    def make[A](data0: Data[A], data1: Data[A]): Update =
+      if (data0.eq(data1)) empty
+      else {
+        val delete = List.from(for ((x, y) <- data0.iterator if !data1.get(x).contains(y)) yield x)
+        val insert = List.from(for ((x, y) <- data1.iterator if !data0.get(x).contains(y)) yield x)
+        val domain = delete.toSet ++ insert
+        Update(domain = domain, delete = delete, insert = insert)
+      }
+  }
+
+  sealed case class Update(
+    domain: Set[String] = Set.empty,
+    delete: List[String] = Nil,
+    insert: List[String] = Nil
+  ) {
+    def deletes: Boolean = delete.nonEmpty
+    def inserts: Boolean = insert.nonEmpty
+    def defined: Boolean = deletes || inserts
+  }
+
+
   /* proper values */
 
   def proper_bool(b: Boolean): Option[Boolean] =