# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1700663979 -3600
# Node ID ef76705bf40205c8fee39b6e3eb167d3af0063e7
# Parent  4df053d29215c91951de34e0ab9dd0de266ce11f
clarified ready vs. next ready;

diff -r 4df053d29215 -r ef76705bf402 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Nov 22 15:04:29 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Nov 22 15:39:39 2023 +0100
@@ -216,7 +216,8 @@
       copy(serial = serial + 1)
     }
 
-    def ready: State.Pending = pending.filter(entry => entry.is_ready && !is_running(entry.name))
+    def ready: State.Pending = pending.filter(_.is_ready)
+    def next_ready: State.Pending = ready.filter(entry => !is_running(entry.name))
 
     def remove_pending(name: String): State =
       copy(pending = pending.flatMap(
@@ -978,7 +979,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.ready.sortBy(_.name)(state.sessions.ordering).take(limit).map(_.name)
+    if (limit > 0) state.next_ready.sortBy(_.name)(state.sessions.ordering).take(limit).map(_.name)
     else Nil
   }
 
diff -r 4df053d29215 -r ef76705bf402 src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Wed Nov 22 15:04:29 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Wed Nov 22 15:39:39 2023 +0100
@@ -430,17 +430,17 @@
         host_infos.hosts.sorted(host_infos.host_speeds).reverse.map(_ -> max_threads)
 
       val fully_parallelizable =
-        parallel_paths(state.ready.map(_.name).toSet) <= resources.unused_nodes(max_threads).length
+        parallel_paths(state.next_ready.map(_.name).toSet) <= resources.unused_nodes(max_threads).length
 
       if (fully_parallelizable) {
-        val all_tasks = state.ready.map(task => (task, best_threads(task), best_threads(task)))
+        val all_tasks = state.next_ready.map(task => (task, best_threads(task), best_threads(task)))
         resources.try_allocate_tasks(ordered_hosts, all_tasks)._1
       }
       else {
-        val critical_nodes = state.ready.toSet.flatMap(task => critical_path_nodes(task.name))
+        val critical_nodes = state.next_ready.toSet.flatMap(task => critical_path_nodes(task.name))
 
         val (critical, other) =
-          state.ready.sortBy(task => remaining_time_ms(task.name)).reverse.partition(task =>
+          state.next_ready.sortBy(task => remaining_time_ms(task.name)).reverse.partition(task =>
             critical_nodes.contains(task.name))
 
         val critical_tasks = critical.map(task => (task, best_threads(task), best_threads(task)))
@@ -617,10 +617,10 @@
     override def next_jobs(state: Build_Process.State): List[String] = {
       val finalize_limit = if (build_context.master) Int.MaxValue else 0
 
-      if (progress.stopped) state.ready.map(_.name).take(finalize_limit)
+      if (progress.stopped) state.next_ready.map(_.name).take(finalize_limit)
       else if (cache.is_current(state)) cache.configs.map(_.job_name).filterNot(state.is_running)
       else {
-        val current = state.ready.filter(task => is_current(state, task.name))
+        val current = state.next_ready.filter(task => is_current(state, task.name))
         if (current.nonEmpty) current.map(_.name).take(finalize_limit)
         else {
           val start = Time.now()