# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1699526948 -3600
# Node ID f72f576fea3ea9ed21ee5bf308f176ca42550e5f
# Parent  df323f23dfdeacac347b18fa607030caeb08d213
performance tuning for build schedule: faster stopping;

diff -r df323f23dfde -r f72f576fea3e src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Thu Nov 09 11:41:19 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Thu Nov 09 11:49:08 2023 +0100
@@ -553,7 +553,9 @@
     }
 
     override def next_jobs(state: Build_Process.State): List[String] =
-      if (cache.is_current(state)) cache.configs.map(_.job_name)
+      if (progress.stopped)
+        state.pending.filter(entry => entry.is_ready && !state.is_running(entry.name)).map(_.name)
+      else if (cache.is_current(state)) cache.configs.map(_.job_name)
       else {
         val start = Time.now()
         val next = scheduler.next(state)