remove terminated jobs, even if futures do not complete;
authorFabian Huch <huch@in.tum.de>
Wed, 21 Aug 2024 13:33:19 +0200
changeset 80731 834849b55910
parent 80730 be4c1fbccfe8
child 80733 17d8b3f6d744
remove terminated jobs, even if futures do not complete;
src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Tue Aug 20 17:28:51 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Wed Aug 21 13:33:19 2024 +0200
@@ -811,7 +811,7 @@
       }
 
       def update: (State, Map[String, Process_Result]) = {
-        val finished =
+        val finished0 =
           for ((name, future) <- result_futures if future.is_finished)
           yield name ->
             (future.join_result match {
@@ -819,11 +819,20 @@
               case Exn.Exn(exn) => Process_Result(Process_Result.RC.interrupt).error(exn.getMessage)
             })
 
+        val (terminated, cancelling_until1) =
+          cancelling_until
+            .filterNot((name, _) => finished0.contains(name))
+            .partition((name, _) => do_terminate(name))
+
+        val finished =
+          finished0 ++
+            terminated.map((name, _) => name -> Process_Result(Process_Result.RC.timeout))
+
         val state1 =
           copy(
             process_futures.filterNot((name, _) => finished.contains(name)),
             result_futures.filterNot((name, _) => finished.contains(name)),
-            cancelling_until.filterNot((name, _) => finished.contains(name) || do_terminate(name)))
+            cancelling_until1)
         (state1, finished)
       }