--- a/src/Pure/Tools/build_job.scala Thu Mar 02 13:19:21 2023 +0100
+++ b/src/Pure/Tools/build_job.scala Thu Mar 02 13:26:46 2023 +0100
@@ -40,6 +40,13 @@
def is_session_name(job_name: String): Boolean = !Long_Name.is_qualified(job_name)
+ def start_session(
+ build_context: Build_Process.Context,
+ session_background: Sessions.Background,
+ input_shasum: SHA1.Shasum,
+ node_info: Node_Info
+ ): Session_Job = new Session_Job(build_context, session_background, input_shasum, node_info)
+
object Session_Context {
def load(
name: String,
@@ -94,7 +101,7 @@
override def toString: String = name
}
- class Session_Job(
+ class Session_Job private[Build_Job](
build_context: Build_Process.Context,
session_background: Sessions.Background,
input_shasum: SHA1.Shasum,
--- a/src/Pure/Tools/build_process.scala Thu Mar 02 13:19:21 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Thu Mar 02 13:26:46 2023 +0100
@@ -601,7 +601,7 @@
val (numa_node, state1) = state.numa_next(build_context.numa_nodes)
val node_info = Build_Job.Node_Info(build_context.hostname, numa_node)
val job =
- new Build_Job.Session_Job(
+ Build_Job.start_session(
build_context, build_deps.background(session_name), input_shasum, node_info)
state1.add_running(session_name, job)
}