# HG changeset patch
# User wenzelm
# Date 1709993662 -3600
# Node ID a9da5e99e22f96dcab1b4fa48a0c23f0776f96a5
# Parent  5969ead9f9007782683b923e3b5225d6bd2856e2
tuned signature;

diff -r 5969ead9f900 -r a9da5e99e22f src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Sat Mar 09 14:52:28 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Sat Mar 09 15:14:22 2024 +0100
@@ -40,6 +40,14 @@
     serial: Long
   )
 
+  object Task {
+    type Entry = (String, Task)
+    def entry(name: String, deps: List[String], build_uuid: String): Entry =
+      name -> Task(name, deps, build_uuid)
+    def entry(session: Build_Job.Session_Context, build_context: isabelle.Build.Context): Entry =
+      entry(session.name, session.deps, build_context.build_uuid)
+  }
+
   sealed case class Task(
     name: String,
     deps: List[String],
@@ -582,7 +590,7 @@
           val name = res.string(Pending.name)
           val deps = res.string(Pending.deps)
           val build_uuid = res.string(Pending.build_uuid)
-          name -> Task(name, split_lines(deps), build_uuid)
+          Task.entry(name, split_lines(deps), build_uuid)
         })
 
     def update_pending(
@@ -981,7 +989,7 @@
       sessions1.iterator.foldLeft(state.pending) {
         case (map, session) =>
           if (map.isDefinedAt(session.name)) map
-          else map + (session.name -> Build_Process.Task(session.name, session.deps, build_uuid))
+          else map + Build_Process.Task.entry(session, build_context)
       }
     state.copy(sessions = sessions1, pending = pending1)
   }
diff -r 5969ead9f900 -r a9da5e99e22f src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Sat Mar 09 14:52:28 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Sat Mar 09 15:14:22 2024 +0100
@@ -1329,12 +1329,10 @@
       val timing_data = Timing_Data.load(host_infos, log_database)
 
       val sessions = Build_Process.Sessions.empty.init(build_context, database_server, progress)
-      def task(session: Build_Job.Session_Context): Build_Process.Task =
-        Build_Process.Task(session.name, session.deps, build_context.build_uuid)
 
       val build_state =
         Build_Process.State(sessions = sessions,
-          pending = sessions.iterator.map(session => (session.name -> task(session))).toMap)
+          pending = Map.from(sessions.iterator.map(Build_Process.Task.entry(_, build_context))))
 
       val scheduler = Build_Engine.scheduler(timing_data, build_context)
       def schedule_msg(res: Exn.Result[Schedule]): String =