# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1701460440 -3600
# Node ID ed00312f694fa75c8d3eaf677defb3b67c0e963f
# Parent  f5a2f956b53122fa16f0ccd65f3dd1b1771bca12
tuned;

diff -r f5a2f956b531 -r ed00312f694f src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Fri Dec 01 20:53:05 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Fri Dec 01 20:54:00 2023 +0100
@@ -823,10 +823,11 @@
 
   class Engine extends Build.Engine("build_schedule") {
 
-    def scheduler(timing_data: Timing_Data, sessions_structure: Sessions.Structure): Scheduler = {
+    def scheduler(timing_data: Timing_Data, context: Build.Context): Scheduler = {
+      val sessions_structure = context.sessions_structure
       val heuristics =
-        List(5, 10, 20).map(minutes =>
-          Timing_Heuristic(Time.minutes(minutes), timing_data, sessions_structure))
+        List(5, 10, 20).map(Time.minutes(_)).map(
+          Timing_Heuristic(_, timing_data, sessions_structure))
       new Meta_Heuristic(heuristics)
     }
 
@@ -836,8 +837,7 @@
       server: SSH.Server
     ): Build_Process =
       new Scheduled_Build_Process(context, progress, server) {
-        def init_scheduler(timing_data: Timing_Data): Scheduler =
-          scheduler(timing_data, context.sessions_structure)
+        def init_scheduler(timing_data: Timing_Data): Scheduler = scheduler(timing_data, context)
       }
   }
 
@@ -907,7 +907,7 @@
       val build_state =
         Build_Process.State(sessions = sessions, pending = sessions.iterator.map(task).toList)
 
-      val scheduler = build_engine.scheduler(timing_data, build_context.sessions_structure)
+      val scheduler = build_engine.scheduler(timing_data, build_context)
       def schedule_msg(res: Exn.Result[Schedule]): String =
         res match { case Exn.Res(schedule) => schedule.message case _ => "" }