# HG changeset patch
# User wenzelm
# Date 1717705600 -7200
# Node ID cff00b3dddf56cd166c3e40501f83482d9c17138
# Parent  f55a11cd3b71d1eb8b44b6b95e1c5348249fc126
clarified names;

diff -r f55a11cd3b71 -r cff00b3dddf5 etc/build.props
--- a/etc/build.props	Thu Jun 06 22:34:24 2024 +0200
+++ b/etc/build.props	Thu Jun 06 22:26:40 2024 +0200
@@ -243,6 +243,7 @@
   src/Pure/term.scala \
   src/Pure/term_xml.scala \
   src/Pure/thm_name.scala \
+  src/Pure/update.scala \
   src/Tools/Graphview/graph_file.scala \
   src/Tools/Graphview/graph_panel.scala \
   src/Tools/Graphview/graphview.scala \
diff -r f55a11cd3b71 -r cff00b3dddf5 src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Thu Jun 06 22:34:24 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Thu Jun 06 22:26:40 2024 +0200
@@ -328,8 +328,8 @@
       db: SQL.Database,
       old_pending: Build_Manager.State.Pending,
       pending: Build_Manager.State.Pending
-    ): Library.Update = {
-      val update = Library.Update.make(old_pending, pending)
+    ): Update = {
+      val update = Update.make(old_pending, pending)
       val delete = update.delete.map(old_pending(_).id.toString)
 
       if (update.deletes)
@@ -410,8 +410,8 @@
       db: SQL.Database,
       old_running: Build_Manager.State.Running,
       running: Build_Manager.State.Running
-    ): Library.Update = {
-      val update = Library.Update.make(old_running, running)
+    ): Update = {
+      val update = Update.make(old_running, running)
       val delete = update.delete.map(old_running(_).id.toString)
 
       if (update.deletes)
diff -r f55a11cd3b71 -r cff00b3dddf5 src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Thu Jun 06 22:34:24 2024 +0200
+++ b/src/Pure/Build/build_process.scala	Thu Jun 06 22:26:40 2024 +0200
@@ -109,11 +109,11 @@
           })
       }
 
-    def update(updates: List[Library.Update.Op[Build_Job.Session_Context]]): Sessions = {
+    def update(updates: List[Update.Op[Build_Job.Session_Context]]): Sessions = {
       val graph1 =
         updates.foldLeft(graph) {
-          case (g, Library.Update.Delete(name)) => g.del_node(name)
-          case (g, Library.Update.Insert(session)) =>
+          case (g, Update.Delete(name)) => g.del_node(name)
+          case (g, Update.Insert(session)) =>
             (if (g.defined(session.name)) g.del_node(session.name) else g)
               .new_node(session.name, session)
         }
@@ -384,7 +384,7 @@
       build_id: Long,
       serial_seen: Long,
       get: SQL.Result => A
-    ): List[Library.Update.Op[A]] = {
+    ): List[Update.Op[A]] = {
       val domain_columns = List(Updates.dom_name)
       val domain_table =
         SQL.Table("domain", domain_columns, body =
@@ -401,17 +401,17 @@
           domain_table.query_named + SQL.join_outer + table +
             " ON " + Updates.dom + " = " + Generic.name)
 
-      db.execute_query_statement(select_sql, List.from[Library.Update.Op[A]],
+      db.execute_query_statement(select_sql, List.from[Update.Op[A]],
         res =>
-          if (res.bool(Updates.delete)) Library.Update.Delete(res.string(Updates.name))
-          else Library.Update.Insert(get(res)))
+          if (res.bool(Updates.delete)) Update.Delete(res.string(Updates.name))
+          else Update.Insert(get(res)))
     }
 
     def write_updates(
       db: SQL.Database,
       build_id: Long,
       serial: Long,
-      updates: List[Library.Update]
+      updates: List[Update]
     ): Unit =
       db.execute_batch_statement(db.insert_permissive(Updates.table), batch =
         for (update <- updates.iterator; kind = update.kind; name <- update.domain.iterator)
@@ -568,10 +568,10 @@
       db: SQL.Database,
       sessions: Build_Process.Sessions,
       old_sessions: Build_Process.Sessions
-    ): Library.Update = {
+    ): Update = {
       val update =
-        if (old_sessions.eq(sessions)) Library.Update.empty
-        else Library.Update.make(old_sessions.data, sessions.data, kind = Sessions.table_index)
+        if (old_sessions.eq(sessions)) Update.empty
+        else Update.make(old_sessions.data, sessions.data, kind = Sessions.table_index)
 
       if (update.deletes) {
         db.execute_statement(
@@ -706,7 +706,7 @@
     }
 
     def pull_pending(db: SQL.Database, build_id: Long, state: State): State.Pending =
-      Library.Update.data(state.pending,
+      Update.data(state.pending,
         read_updates(db, Pending.table, build_id, state.serial,
           { res =>
             val name = res.string(Pending.name)
@@ -720,8 +720,8 @@
       db: SQL.Database,
       pending: State.Pending,
       old_pending: State.Pending
-    ): Library.Update = {
-      val update = Library.Update.make(old_pending, pending, kind = Pending.table_index)
+    ): Update = {
+      val update = Update.make(old_pending, pending, kind = Pending.table_index)
 
       if (update.deletes) {
         db.execute_statement(
@@ -762,7 +762,7 @@
     }
 
     def pull_running(db: SQL.Database, build_id: Long, state: State): State.Running =
-      Library.Update.data(state.running,
+      Update.data(state.running,
         read_updates(db, Running.table, build_id, state.serial,
           { res =>
             val name = res.string(Running.name)
@@ -782,8 +782,8 @@
       db: SQL.Database,
       running: State.Running,
       old_running: State.Running
-    ): Library.Update = {
-      val update = Library.Update.make(old_running, running, kind = Running.table_index)
+    ): Update = {
+      val update = Update.make(old_running, running, kind = Running.table_index)
 
       if (update.deletes) {
         db.execute_statement(
@@ -837,7 +837,7 @@
     }
 
     def pull_results(db: SQL.Database, build_id: Long, state: State): State.Results =
-      Library.Update.data(state.results,
+      Update.data(state.results,
         read_updates(db, Results.table, build_id, state.serial,
           { res =>
             val name = res.string(Results.name)
@@ -876,8 +876,8 @@
       db: SQL.Database,
       results: State.Results,
       old_results: State.Results
-    ): Library.Update = {
-      val update = Library.Update.make(old_results, results, kind = Results.table_index)
+    ): Update = {
+      val update = Update.make(old_results, results, kind = Results.table_index)
 
       if (update.deletes) {
         db.execute_statement(
diff -r f55a11cd3b71 -r cff00b3dddf5 src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Thu Jun 06 22:34:24 2024 +0200
+++ b/src/Pure/Build/build_schedule.scala	Thu Jun 06 22:26:40 2024 +0200
@@ -1363,7 +1363,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 = Library.Update.make(read_scheduled_builds_domain(db), running_builds_domain)
+      val update = Update.make(read_scheduled_builds_domain(db), running_builds_domain)
 
       remove_schedules(db, update.delete)
     }
diff -r f55a11cd3b71 -r cff00b3dddf5 src/Pure/library.scala
--- a/src/Pure/library.scala	Thu Jun 06 22:34:24 2024 +0200
+++ b/src/Pure/library.scala	Thu Jun 06 22:26:40 2024 +0200
@@ -285,42 +285,6 @@
     }
 
 
-  /* data update */
-
-  object Update {
-    sealed abstract class Op[A]
-    case class Delete[A](name: String) extends Op[A]
-    case class Insert[A](item: A) extends Op[A]
-
-    def data[A <: Name.T](old_data: Name.Data[A], updates: List[Op[A]]): Name.Data[A] =
-      updates.foldLeft(old_data) {
-        case (map, Delete(name)) => map - name
-        case (map, Insert(item)) => map + (item.name -> item)
-      }
-
-    val empty: Update = Update()
-
-    def make[A](a: Name.Data[A], b: Name.Data[A], kind: Int = 0): Update =
-      if (a eq b) empty
-      else {
-        val delete = List.from(for ((x, y) <- a.iterator if !b.get(x).contains(y)) yield x)
-        val insert = List.from(for ((x, y) <- b.iterator if !a.get(x).contains(y)) yield x)
-        Update(delete = delete, insert = insert, kind = kind)
-      }
-  }
-
-  sealed case class Update(
-    delete: List[String] = Nil,
-    insert: List[String] = Nil,
-    kind: Int = 0
-  ) {
-    def deletes: Boolean = delete.nonEmpty
-    def inserts: Boolean = insert.nonEmpty
-    def defined: Boolean = deletes || inserts
-    lazy val domain: Set[String] = delete.toSet ++ insert
-  }
-
-
   /* proper values */
 
   def proper_bool(b: Boolean): Option[Boolean] =
diff -r f55a11cd3b71 -r cff00b3dddf5 src/Pure/update.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/update.scala	Thu Jun 06 22:26:40 2024 +0200
@@ -0,0 +1,41 @@
+/*  Title:      Pure/update.scala
+    Author:     Makarius
+
+Update data (with formal name).
+*/
+
+package isabelle
+
+
+object Update {
+  sealed abstract class Op[A]
+  case class Delete[A](name: String) extends Op[A]
+  case class Insert[A](item: A) extends Op[A]
+
+  def data[A <: Name.T](old_data: Name.Data[A], updates: List[Op[A]]): Name.Data[A] =
+    updates.foldLeft(old_data) {
+      case (map, Delete(name)) => map - name
+      case (map, Insert(item)) => map + (item.name -> item)
+    }
+
+  val empty: Update = Update()
+
+  def make[A](a: Name.Data[A], b: Name.Data[A], kind: Int = 0): Update =
+    if (a eq b) empty
+    else {
+      val delete = List.from(for ((x, y) <- a.iterator if !b.get(x).contains(y)) yield x)
+      val insert = List.from(for ((x, y) <- b.iterator if !a.get(x).contains(y)) yield x)
+      Update(delete = delete, insert = insert, kind = kind)
+    }
+}
+
+sealed case class Update(
+  delete: List[String] = Nil,
+  insert: List[String] = Nil,
+  kind: Int = 0
+) {
+  def deletes: Boolean = delete.nonEmpty
+  def inserts: Boolean = insert.nonEmpty
+  def defined: Boolean = deletes || inserts
+  lazy val domain: Set[String] = delete.toSet ++ insert
+}