# 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 + } } }