# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1699894091 -3600
# Node ID 4a5d35b35aeb9ff240676b30c3f2b8c9b0691d27
# Parent  9e963cd24fd287aaca32187eef765d4b443a5e09
better invalidation for schedule cache (only on relevant changes);

diff -r 9e963cd24fd2 -r 4a5d35b35aeb src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Mon Nov 13 17:31:37 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Mon Nov 13 17:48:11 2023 +0100
@@ -576,9 +576,10 @@
     /* build process */
 
     case class Cache(state: Build_Process.State, configs: List[Config], estimate: Date) {
-      def is_current(state: Build_Process.State): Boolean = this.state == state
+      def is_current(state: Build_Process.State): Boolean =
+        this.state.pending.nonEmpty && this.state.results == state.results
       def is_current_estimate(estimate: Date): Boolean =
-        this.estimate.time - estimate.time >= Time.seconds(1)
+        Math.abs((this.estimate.time - estimate.time).ms) < Time.minutes(1).ms
     }
 
     private var cache = Cache(Build_Process.State(), Nil, Date.now())
@@ -617,7 +618,7 @@
       val finalize_limit = if (build_context.master) Int.MaxValue else 0
 
       if (progress.stopped) state.ready.map(_.name).take(finalize_limit)
-      else if (cache.is_current(state)) cache.configs.map(_.job_name)
+      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))
         if (current.nonEmpty) current.map(_.name).take(finalize_limit)