# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1700661869 -3600
# Node ID 4df053d29215c91951de34e0ab9dd0de266ce11f
# Parent  7449ff77029eef83646f1fc527d43829a07fb769
introduced path heuristic abstraction;

diff -r 7449ff77029e -r 4df053d29215 src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Wed Nov 22 17:50:36 2023 +0000
+++ b/src/Pure/Tools/build_schedule.scala	Wed Nov 22 15:04:29 2023 +0100
@@ -324,6 +324,8 @@
   }
 
   abstract class Heuristic(timing_data: Timing_Data) extends Scheduler {
+    val host_infos = timing_data.host_infos
+
     def build_duration(build_state: Build_Process.State): Time = {
       @tailrec
       def simulate(state: State): State =
@@ -352,12 +354,8 @@
 
   /* heuristics */
 
-  class Timing_Heuristic(
-    threshold: Time,
-    timing_data: Timing_Data,
-    sessions_structure: Sessions.Structure,
-    max_threads: Int = 8
-  ) extends Heuristic(timing_data) {
+  abstract class Path_Heuristic(timing_data: Timing_Data, sessions_structure: Sessions.Structure)
+    extends Heuristic(timing_data) {
     /* pre-computed properties for efficient heuristic */
 
     type Node = String
@@ -383,10 +381,6 @@
         .groupMapReduce(_._1)(_._2)(_ max _)
     }
 
-    val critical_path_nodes =
-      build_graph.keys.map(node =>
-        node -> path_times(node).filter((_, time) => time > threshold).keySet).toMap
-
     def parallel_paths(minimals: Set[Node], pred: Node => Boolean = _ => true): Int = {
       def start(node: Node): (Node, Time) = node -> best_times(node)
 
@@ -413,11 +407,17 @@
 
       parallel_paths(minimals.map(start).toMap)._1
     }
-
+  }
 
-    /* scheduling */
-
-    val host_infos = timing_data.host_infos
+  class Timing_Heuristic(
+    threshold: Time,
+    timing_data: Timing_Data,
+    sessions_structure: Sessions.Structure,
+    max_threads: Int = 8
+  ) extends Path_Heuristic(timing_data, sessions_structure) {
+    val critical_path_nodes =
+      build_graph.keys.map(node =>
+        node -> path_times(node).filter((_, time) => time > threshold).keySet).toMap
 
     def next(state: Build_Process.State): List[Config] = {
       val resources = host_infos.available(state)