# HG changeset patch
# User wenzelm
# Date 1709995709 -3600
# Node ID d014b6c40eb0e5c188d42a754e0087e66c5b2e2d
# Parent  a9da5e99e22f96dcab1b4fa48a0c23f0776f96a5
misc tuning and clarification;

diff -r a9da5e99e22f -r d014b6c40eb0 src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Sat Mar 09 15:14:22 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Sat Mar 09 15:48:29 2024 +0100
@@ -220,10 +220,12 @@
     results: State.Results = Map.empty
   ) {
     require(serial >= 0, "serial underflow")
-    def inc_serial: State = {
+
+    def next_serial: Long = {
       require(serial < Long.MaxValue, "serial overflow")
-      copy(serial = serial + 1)
+      serial + 1
     }
+    def inc_serial: State = copy(serial = next_serial)
 
     def ready: List[Task] = pending.valuesIterator.filter(_.is_ready).toList.sortBy(_.name)
     def next_ready: List[Task] = ready.filter(entry => !is_running(entry.name))
@@ -822,17 +824,20 @@
       state: State,
       old_state: State
     ): State = {
+      val serial = state.next_serial
       val changed =
         List(
           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))
+          update_results(db, state.results, old_state.results)
+        ).exists(identity)
 
-      val state1 = if (changed.exists(identity)) state.inc_serial else state
-      if (state1.serial != state.serial) stamp_worker(db, worker_uuid, state1.serial)
-
-      state1
+      if (changed) {
+        stamp_worker(db, worker_uuid, serial)
+        state.copy(serial = serial)
+      }
+      else state
     }
   }