# HG changeset patch
# User wenzelm
# Date 1710001389 -3600
# Node ID 866d96915388cb6d483847242d4ba49c940f01d1
# Parent  45b81ff3c97244e15dea949d7dbc86fd2f1f43d2
clarified modules;

diff -r 45b81ff3c972 -r 866d96915388 src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Sat Mar 09 16:59:38 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Sat Mar 09 17:23:09 2024 +0100
@@ -213,6 +213,11 @@
     results: State.Results)     // finished results
 
   object State {
+    def inc_serial(serial: Long) = {
+      require(serial < Long.MaxValue, "serial overflow")
+      serial + 1
+    }
+
     type Pending = Map[String, Task]
     type Running = Map[String, Job]
     type Results = Map[String, Result]
@@ -228,10 +233,7 @@
   ) {
     require(serial >= 0, "serial underflow")
 
-    def next_serial: Long = {
-      require(serial < Long.MaxValue, "serial overflow")
-      serial + 1
-    }
+    def next_serial: Long = State.inc_serial(serial)
     def inc_serial: State = copy(serial = next_serial)
 
     def ready: List[Task] = pending.valuesIterator.filter(_.is_ready).toList.sortBy(_.name)
diff -r 45b81ff3c972 -r 866d96915388 src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Sat Mar 09 16:59:38 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Sat Mar 09 17:23:09 2024 +0100
@@ -469,11 +469,9 @@
     serial: Long = 0,
   ) {
     require(serial >= 0, "serial underflow")
-    def inc_serial: Schedule = {
-      require(serial < Long.MaxValue, "serial overflow")
-      copy(serial = serial + 1)
-    }
-    
+
+    def next_serial: Long = Build_Process.State.inc_serial(serial)
+
     def end: Date =
       if (graph.is_empty) start
       else graph.maximals.map(graph.get_node).map(_.end).maxBy(_.unix_epoch)
@@ -1191,7 +1189,7 @@
         schedule.graph != old_schedule.graph
       
       val schedule1 =
-        if (changed) schedule.copy(serial = old_schedule.serial).inc_serial else schedule
+        if (changed) schedule.copy(serial = old_schedule.next_serial) else schedule
       if (schedule1.serial != schedule.serial) write_schedule(db, schedule1)
       
       schedule1