--- 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 \
--- 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)
--- 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(
--- 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)
}
--- 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] =
--- /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
+}