--- a/src/Pure/Build/build_process.scala Mon Mar 11 21:46:31 2024 +0100
+++ b/src/Pure/Build/build_process.scala Fri Mar 15 19:15:04 2024 +0100
@@ -911,7 +911,7 @@
/* collective operations */
- def pull_database(db: SQL.Database, build_id: Long, worker_uuid: String, state: State): State = {
+ def pull_state(db: SQL.Database, build_id: Long, worker_uuid: String, state: State): State = {
val serial_db = read_serial(db)
if (serial_db == state.serial) state
else {
@@ -928,7 +928,7 @@
}
}
- def update_database(
+ def push_state(
db: SQL.Database,
build_id: Long,
worker_uuid: String,
@@ -1124,11 +1124,11 @@
case Some(db) =>
Build_Process.private_data.transaction_lock(db, label = label) {
val old_state =
- Build_Process.private_data.pull_database(db, build_id, worker_uuid, _state)
+ Build_Process.private_data.pull_state(db, build_id, worker_uuid, _state)
_state = old_state
val res = body
_state =
- Build_Process.private_data.update_database(
+ Build_Process.private_data.push_state(
db, build_id, worker_uuid, _state, old_state)
res
}
--- a/src/Pure/Build/build_schedule.scala Mon Mar 11 21:46:31 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala Fri Mar 15 19:15:04 2024 +0100
@@ -879,15 +879,15 @@
case Some(db) =>
db.transaction_lock(Build_Schedule.private_data.all_tables, label = label) {
val old_state =
- Build_Process.private_data.pull_database(db, build_id, worker_uuid, _state)
+ Build_Process.private_data.pull_state(db, build_id, worker_uuid, _state)
val old_schedule = Build_Schedule.private_data.pull_schedule(db, _schedule)
_state = old_state
_schedule = old_schedule
val res = body
_state =
- Build_Process.private_data.update_database(
+ Build_Process.private_data.push_state(
db, build_id, worker_uuid, _state, old_state)
- _schedule = Build_Schedule.private_data.update_schedule(db, _schedule, old_schedule)
+ _schedule = Build_Schedule.private_data.pull_schedule(db, _schedule, old_schedule)
res
}
}
@@ -1273,7 +1273,7 @@
}
}
- def update_schedule(db: SQL.Database, schedule: Schedule, old_schedule: Schedule): Schedule = {
+ def pull_schedule(db: SQL.Database, schedule: Schedule, old_schedule: Schedule): Schedule = {
val changed =
schedule.generator != old_schedule.generator ||
schedule.start != old_schedule.start ||