# HG changeset patch
# User wenzelm
# Date 1677702248 -3600
# Node ID ecfe6dac3a3ef81e6e50656e86acb095c66fa52e
# Parent  8008ce0f2488a13e1a5c41c3b25ddd14a6a6ef54
simplified startup under "locked" condition (in contrast to f7e413e8d269);

diff -r 8008ce0f2488 -r ecfe6dac3a3e src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Wed Mar 01 21:15:20 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Wed Mar 01 21:24:08 2023 +0100
@@ -14,7 +14,6 @@
 trait Build_Job {
   def job_name: String
   def node_info: Build_Job.Node_Info
-  def start(): Unit = ()
   def terminate(): Unit = ()
   def is_finished: Boolean = false
   def finish: (Process_Result, SHA1.Shasum) = (Process_Result.undefined, SHA1.no_shasum)
@@ -117,7 +116,7 @@
     val session_sources: Sessions.Sources =
       Sessions.Sources.load(session_background.base, cache = store.cache.compress)
 
-    private lazy val future_result: Future[Process_Result] =
+    private val future_result: Future[Process_Result] =
       Future.thread("build", uninterruptible = true) {
         val env =
           Isabelle_System.settings(
@@ -420,7 +419,6 @@
         }
       }
 
-    override def start(): Unit = future_result
     override def terminate(): Unit = future_result.cancel()
     override def is_finished: Boolean = future_result.is_finished
 
diff -r 8008ce0f2488 -r ecfe6dac3a3e src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Mar 01 21:15:20 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Mar 01 21:24:08 2023 +0100
@@ -624,17 +624,15 @@
         new Resources(session_background, log = log,
           command_timings = build_context.old_command_timings(session_name))
 
-      val job =
-        synchronized {
-          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_context, session_background, session_heaps,
-              store_heap, resources, input_shasum, node_info)
-          _state = state1.add_running(session_name, job)
-          job
-        }
-      job.start()
+      synchronized {
+        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_context, session_background, session_heaps,
+            store_heap, resources, input_shasum, node_info)
+        _state = state1.add_running(session_name, job)
+        job
+      }
     }
   }