# HG changeset patch # User wenzelm # Date 1677760006 -3600 # Node ID 5ecaf881b5634d5d0858c240a4a7ec961b2a5a06 # Parent 362bf802013ec67c4a2bf0dfe175a28a813ad4f3 clarified signature; diff -r 362bf802013e -r 5ecaf881b563 src/Pure/Tools/build_job.scala --- 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, diff -r 362bf802013e -r 5ecaf881b563 src/Pure/Tools/build_process.scala --- 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) }