# HG changeset patch # User wenzelm # Date 1678786037 -3600 # Node ID 739cb777cc758d2e1a8adc627c805332c62911c9 # Parent e79a5ce8a74c4f5c9b1cb80dbd577fd4492391c6 clarified signature; diff -r e79a5ce8a74c -r 739cb777cc75 src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Tue Mar 14 10:16:45 2023 +0100 +++ b/src/Pure/Tools/build_job.scala Tue Mar 14 10:27:17 2023 +0100 @@ -11,7 +11,6 @@ trait Build_Job { - def node_info: Host.Node_Info def cancel(): Unit = () def is_finished: Boolean = false def join: (Process_Result, SHA1.Shasum) = (Process_Result.undefined, SHA1.no_shasum) @@ -103,7 +102,7 @@ log: Logger, session_background: Sessions.Background, input_shasum: SHA1.Shasum, - override val node_info: Host.Node_Info + node_info: Host.Node_Info ) extends Build_Job { private val store = build_context.store diff -r e79a5ce8a74c -r 739cb777cc75 src/Pure/Tools/build_process.scala --- a/src/Pure/Tools/build_process.scala Tue Mar 14 10:16:45 2023 +0100 +++ b/src/Pure/Tools/build_process.scala Tue Mar 14 10:27:17 2023 +0100 @@ -248,10 +248,10 @@ def stop_running(): Unit = for (job <- running.valuesIterator; build <- job.build) build.cancel() - def finished_running(): List[(String, Build_Job)] = + def finished_running(): List[Job] = List.from( for (job <- running.valuesIterator; build <- job.build if build.is_finished) - yield job.name -> build) + yield job) def add_running(job: Job): State = copy(running = running + (job.name -> job)) @@ -1066,12 +1066,12 @@ synchronized_database { if (progress.stopped) _state.stop_running() - for ((job_name, build) <- _state.finished_running()) { - val (process_result, output_shasum) = build.join + for (job <- _state.finished_running()) { + val (process_result, output_shasum) = job.build.get.join _state = _state. - remove_pending(job_name). - remove_running(job_name). - make_result(job_name, process_result, output_shasum, node_info = build.node_info) + remove_pending(job.name). + remove_running(job.name). + make_result(job.name, process_result, output_shasum, node_info = job.node_info) } }