--- 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)
}
--- 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 =