clarified signature;
authorwenzelm
Thu, 02 Mar 2023 13:26:46 +0100
changeset 77474 5ecaf881b563
parent 77473 362bf802013e
child 77475 3bc611c80346
clarified signature;
src/Pure/Tools/build_job.scala
src/Pure/Tools/build_process.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,
--- 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)
     }