# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1699544376 -3600
# Node ID ae1403e341dd337ec63c91c76b6fe945f082c71a
# Parent  26841d3c568c750c6dc4f24e205c20cecd01915d
tuned;

diff -r 26841d3c568c -r ae1403e341dd src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Thu Nov 09 15:45:51 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Thu Nov 09 16:39:36 2023 +0100
@@ -306,12 +306,8 @@
     def finished: Boolean = build_state.pending.isEmpty && build_state.running.isEmpty
   }
 
-  abstract class Scheduler {
-    def ready_jobs(state: Build_Process.State): Build_Process.State.Pending =
-      state.pending.filter(entry => entry.is_ready && !state.is_running(entry.name))
-
+  trait Scheduler {
     def next(state: Build_Process.State): List[Config]
-
     def build_duration(build_state: Build_Process.State): Time
   }
 
@@ -321,8 +317,7 @@
       def simulate(state: State): State =
         if (state.finished) state
         else {
-          val state1 =
-            next(state.build_state).foldLeft(state)(_.start(_)).step(timing_data)
+          val state1 = next(state.build_state).foldLeft(state)(_.start(_)).step(timing_data)
           simulate(state1)
         }
 
@@ -391,7 +386,7 @@
         timing_data.best_threads(task.name).getOrElse(
           host_infos.hosts.map(_.info.num_cpus).max min 8)
 
-      val ready = ready_jobs(state)
+      val ready = state.pending.filter(entry => entry.is_ready && !state.is_running(entry.name))
       val free = resources.unused_hosts
 
       if (ready.length <= free.length)