# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1699621656 -3600
# Node ID faa5af35fb65ddb598fc66a9c349567af3e2e24b
# Parent  7dec63adda7de53f7e802d1e9fa0c845a6f69224
clarified signature: more operations;

diff -r 7dec63adda7d -r faa5af35fb65 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Mon Nov 13 09:02:56 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Fri Nov 10 14:07:36 2023 +0100
@@ -216,6 +216,8 @@
       copy(serial = serial + 1)
     }
 
+    def ready: State.Pending = pending.filter(entry => entry.is_ready && !is_running(entry.name))
+
     def remove_pending(name: String): State =
       copy(pending = pending.flatMap(
         entry => if (entry.name == name) None else Some(entry.resolve(name))))
@@ -976,11 +978,7 @@
       if (progress.stopped) { if (build_context.master) Int.MaxValue else 0 }
       else build_context.max_jobs - state.build_running.length
     }
-    if (limit > 0) {
-      state.pending.filter(entry => entry.is_ready && !state.is_running(entry.name))
-        .sortBy(_.name)(state.sessions.ordering)
-        .take(limit).map(_.name)
-    }
+    if (limit > 0) state.ready.sortBy(_.name)(state.sessions.ordering).take(limit).map(_.name)
     else Nil
   }
 
diff -r 7dec63adda7d -r faa5af35fb65 src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Mon Nov 13 09:02:56 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Fri Nov 10 14:07:36 2023 +0100
@@ -389,22 +389,21 @@
         timing_data.best_threads(task.name).getOrElse(
           host_infos.hosts.map(_.info.num_cpus).max min 8)
 
-      val ready = state.pending.filter(entry => entry.is_ready && !state.is_running(entry.name))
       val free = resources.unused_hosts
 
-      if (ready.length <= free.length)
-        resources.try_allocate_tasks(free, ready.map(task => task -> best_threads(task)))._1
+      if (state.ready.length <= free.length)
+        resources.try_allocate_tasks(free, state.ready.map(task => task -> best_threads(task)))._1
       else {
         val pending_tasks = state.pending.map(_.name).toSet
 
-        val critical_nodes = ready.toSet.flatMap(task => critical_path_nodes(task.name))
+        val critical_nodes = state.ready.toSet.flatMap(task => critical_path_nodes(task.name))
         def is_critical(node: Node): Boolean = critical_nodes.contains(node)
 
         def parallel_paths(node: Node): Int =
           build_graph.imm_succs(node).filter(is_critical).map(parallel_paths(_) max 1).sum max 1
 
         val (critical, other) =
-          ready.sortBy(task => remaining_time(task.name)).reverse.partition(task =>
+          state.ready.sortBy(task => remaining_time(task.name)).reverse.partition(task =>
             is_critical(task.name))
 
         val (critical_hosts, other_hosts) =
@@ -556,8 +555,7 @@
     }
 
     override def next_jobs(state: Build_Process.State): List[String] =
-      if (progress.stopped)
-        state.pending.filter(entry => entry.is_ready && !state.is_running(entry.name)).map(_.name)
+      if (progress.stopped) state.ready.map(_.name)
       else if (cache.is_current(state)) cache.configs.map(_.job_name)
       else {
         val start = Time.now()