# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1701460293 -3600
# Node ID 91955d607aad24f4b6b4b0eee1496eb294cdec7e
# Parent  6e92475ff925dbb02ff9e01023a49a6d041e521f
proper unused nodes;

diff -r 6e92475ff925 -r 91955d607aad src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Fri Dec 01 20:50:40 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Fri Dec 01 20:51:33 2023 +0100
@@ -337,15 +337,15 @@
     host_infos: Host_Infos,
     allocated_nodes: Map[Host, List[Node_Info]]
   ) {
-    def unused_nodes(threads: Int): List[Node_Info] = {
-      val fully_allocated =
-        host_infos.hosts.foldLeft(this) { case (resources, host) =>
-          if (!resources.available(host, threads)) resources
-          else resources.allocate(resources.next_node(host, threads))
-        }
-      val used_nodes = allocated_nodes.values.flatten.toSet
-      fully_allocated.allocated_nodes.values.flatten.toList.filterNot(used_nodes.contains)
-    }
+    def unused_nodes(host: Host, threads: Int): List[Node_Info] =
+      if (!available(host, threads)) Nil
+      else {
+        val node = next_node(host, threads)
+        node :: allocate(node).unused_nodes(host, threads)
+      }
+
+    def unused_nodes(threads: Int): List[Node_Info] =
+      host_infos.hosts.flatMap(unused_nodes(_, threads))
 
     def allocated(host: Host): List[Node_Info] = allocated_nodes.getOrElse(host, Nil)