src/Pure/Tools/build_process.scala

             timeout, old_time, old_command_timings_blob, build_uuid)
         }
       )
     }
 
-    def update_sessions(db: SQL.Database, sessions: Build_Process.Sessions): Boolean = {
-      val old_sessions = read_sessions_domain(db)
-      val insert = sessions.iterator.filterNot(s => old_sessions.contains(s.name)).toList
+    def update_sessions(
+      db: SQL.Database,
+      sessions: Build_Process.Sessions,
+      old_sessions: Build_Process.Sessions
+    ): Boolean = {
+      val insert = sessions.iterator.filterNot(s => old_sessions.defined(s.name)).toList
 
       if (insert.nonEmpty) {
         db.execute_batch_statement(Sessions.table.insert(), batch =
           for (session <- insert) yield { (stmt: SQL.Statement) =>
             stmt.string(1) = session.name

           val info = res.string(Pending.info)
           val build_uuid = res.string(Pending.build_uuid)
           Task(name, split_lines(deps), JSON.Object.parse(info), build_uuid)
         })
 
-    def update_pending(db: SQL.Database, pending: State.Pending): Boolean = {
-      val old_pending = read_pending(db)
+    def update_pending(
+      db: SQL.Database,
+      pending: State.Pending,
+      old_pending: State.Pending
+    ): Boolean = {
       val (delete, insert) = Library.symmetric_difference(old_pending, pending)
 
       if (delete.nonEmpty) {
         db.execute_statement(
           Pending.table.delete(sql = Generic.sql_where(names = delete.map(_.name))))

           val numa_node = res.get_int(Running.numa_node)
           name -> Job(name, worker_uuid, build_uuid, Host.Node_Info(hostname, numa_node), None)
         }
       )
 
-    def update_running(db: SQL.Database, running: State.Running): Boolean = {
-      val running0 = read_running(db).valuesIterator.toList
+    def update_running(
+      db: SQL.Database,
+      running: State.Running,
+      old_running: State.Running
+    ): Boolean = {
+      val running0 = old_running.valuesIterator.toList
       val running1 = running.valuesIterator.map(_.no_build).toList
       val (delete, insert) = Library.symmetric_difference(running0, running1)
 
       if (delete.nonEmpty) {
         db.execute_statement(

           name ->
             Result(name, worker_uuid, build_uuid, node_info, process_result, output_shasum, current)
         }
       )
 
-    def update_results(db: SQL.Database, results: State.Results): Boolean = {
+    def update_results(
+      db: SQL.Database,
+      results: State.Results,
+      old_results: State.Results
+    ): Boolean = {
       val insert =
-        if (results.isEmpty) Nil
-        else {
-          val old_results = read_results_domain(db)
-          results.valuesIterator.filterNot(res => old_results.contains(res.name)).toList
-        }
+        results.valuesIterator.filterNot(res => old_results.isDefinedAt(res.name)).toList
 
       if (insert.nonEmpty) {
         db.execute_batch_statement(Results.table.insert(), batch =
           for (result <- insert) yield { (stmt: SQL.Statement) =>
             val process_result = result.process_result

         state.copy(serial = serial, sessions = sessions, pending = pending,
           running = running, results = results)
       }
     }
 
-    def update_database(db: SQL.Database, worker_uuid: String, state: State): State = {
+    def update_database(
+      db: SQL.Database,
+      worker_uuid: String,
+      state: State,
+      old_state: State
+    ): State = {
       val changed =
         List(
-          update_sessions(db, state.sessions),
-          update_pending(db, state.pending),
-          update_running(db, state.running),
-          update_results(db, state.results))
+          update_sessions(db, state.sessions, old_state.sessions),
+          update_pending(db, state.pending, old_state.pending),
+          update_running(db, state.running, old_state.running),
+          update_results(db, state.results, old_state.results))
 
       val serial0 = state.serial
       val serial = if (changed.exists(identity)) State.inc_serial(serial0) else serial0
 
       stamp_worker(db, worker_uuid, serial)

     synchronized {
       _build_database match {
         case None => body
         case Some(db) =>
           Build_Process.private_data.transaction_lock(db, label = label) {
-            _state = Build_Process.private_data.pull_database(db, worker_uuid, _state)
+            val old_state = Build_Process.private_data.pull_database(db, worker_uuid, _state)
+            _state = old_state
             val res = body
-            _state = Build_Process.private_data.update_database(db, worker_uuid, _state)
+            _state = Build_Process.private_data.update_database(db, worker_uuid, _state, old_state)
             res
           }
       }
     }