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