# HG changeset patch
# User wenzelm
# Date 1710526504 -3600
# Node ID 1cfc913987d95a5760c7711b4b969d390390bca1
# Parent  d3811cf07da6c1dedb0eb86cc96bec59fea0c7d0
clarified names;

diff -r d3811cf07da6 -r 1cfc913987d9 src/Pure/Build/build_process.scala
--- 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
           }
diff -r d3811cf07da6 -r 1cfc913987d9 src/Pure/Build/build_schedule.scala
--- 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 ||