# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1701360003 -3600
# Node ID 09e27fd11e039a7230fe6b3723bd31b0a2ade567
# Parent  32e839bb622e8132a420c5831971aaf8c763e165
tuned;

diff -r 32e839bb622e -r 09e27fd11e03 src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Thu Nov 30 16:27:27 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Thu Nov 30 17:00:03 2023 +0100
@@ -11,9 +11,6 @@
 
 
 object Build_Schedule {
-  val engine_name = "build_schedule"
-
-
   /* organized historic timing information (extracted from build logs) */
 
   case class Timing_Entry(job_name: String, hostname: String, threads: Int, timing: Timing) {
@@ -715,7 +712,7 @@
 
       val meta_info = Build_Log.Meta_Info(props, settings)
       val build_info = Build_Log.Build_Info(sessions.toMap)
-      val log_name = Build_Log.log_filename(engine = engine_name, date = start_date)
+      val log_name = Build_Log.log_filename(engine = build_context.engine.name, date = start_date)
 
       Build_Log.private_data.update_sessions(
         _log_database, _log_store.cache.compress, log_name.file_name, build_info)
@@ -796,22 +793,23 @@
     }
   }
 
-  class Engine extends Build.Engine(engine_name) {
+  class Engine extends Build.Engine("build_schedule") {
+
+    def scheduler(timing_data: Timing_Data, sessions_structure: Sessions.Structure): Scheduler = {
+      val heuristics =
+        List(5, 10, 20).map(minutes =>
+          Timing_Heuristic(Time.minutes(minutes), timing_data, sessions_structure))
+      new Meta_Heuristic(heuristics)
+    }
+
     override def open_build_process(
       context: Build.Context,
       progress: Progress,
       server: SSH.Server
     ): Build_Process =
       new Scheduled_Build_Process(context, progress, server) {
-        def init_scheduler(timing_data: Timing_Data): Scheduler = {
-          val heuristics =
-            List(5, 10, 20).map(minutes =>
-              Timing_Heuristic(
-                Time.minutes(minutes),
-                timing_data,
-                context.build_deps.sessions_structure))
-          new Meta_Heuristic(heuristics)
-        }
+        def init_scheduler(timing_data: Timing_Data): Scheduler =
+          scheduler(timing_data, context.sessions_structure)
       }
   }
 }