# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1701953634 -3600
# Node ID b0491edc1a9f147f65184c62641c9b393d320ec6
# Parent  8cb732d7a98cb56581384a791e997cb86c523143
clarified;

diff -r 8cb732d7a98c -r b0491edc1a9f src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Fri Dec 08 12:11:22 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Thu Dec 07 13:53:54 2023 +0100
@@ -336,10 +336,6 @@
 
   /* offline tracking of job configurations and resource allocations */
 
-  object Config {
-    def from_job(job: Build_Process.Job): Config = Config(job.name, job.node_info)
-  }
-
   case class Config(job_name: String, node_info: Node_Info) {
     def job_of(start_time: Time): Build_Process.Job =
       Build_Process.Job(job_name, "", "", node_info, Date(start_time), None)
@@ -493,16 +489,15 @@
     def is_finished: Boolean = build_state.pending.isEmpty && build_state.running.isEmpty
   }
 
-  trait Scheduler {
-    def next(state: Build_Process.State): List[Config]
-    def build_schedule(build_state: Build_Process.State): Schedule
-  }
+  trait Scheduler { def build_schedule(build_state: Build_Process.State): Schedule }
 
   abstract class Heuristic(timing_data: Timing_Data, build_uuid: String)
     extends Scheduler {
     val host_infos = timing_data.host_infos
     val ordered_hosts = host_infos.hosts.sorted(host_infos.host_speeds)
 
+    def next(state: Build_Process.State): List[Config]
+
     def build_schedule(build_state: Build_Process.State): Schedule = {
       @tailrec
       def simulate(state: State): State =