--- 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)