# HG changeset patch # User wenzelm # Date 1677506999 -3600 # Node ID 19e9cafaafc565df7a20704649a2aaec547fee3b # Parent f7e14f567adf4dc385263e3c75cad30cfe5bc293 clarified signature: works for general Build_Job; diff -r f7e14f567adf -r 19e9cafaafc5 src/Pure/Tools/build_process.scala --- a/src/Pure/Tools/build_process.scala Mon Feb 27 15:02:14 2023 +0100 +++ b/src/Pure/Tools/build_process.scala Mon Feb 27 15:09:59 2023 +0100 @@ -201,12 +201,8 @@ def stop_running(): Unit = running.valuesIterator.foreach(_.terminate()) - def finished_running(): List[Build_Job.Build_Session] = - List.from( - running.valuesIterator.flatMap { - case job: Build_Job.Build_Session if job.is_finished => Some(job) - case _ => None - }) + def finished_running(): List[Build_Job] = + List.from(running.valuesIterator.filter(_.is_finished)) def add_running(name: String, job: Build_Job): State = copy(running = running + (name -> job)) @@ -537,7 +533,7 @@ protected def stop_running(): Unit = synchronized { _state.stop_running() } - protected def finished_running(): List[Build_Job.Build_Session] = synchronized { + protected def finished_running(): List[Build_Job] = synchronized { _state.finished_running() } @@ -659,14 +655,13 @@ if (progress.stopped) stop_running() for (job <- finished_running()) { - val session_name = job.session_name + val job_name = job.job_name val (process_result, output_heap) = job.finish synchronized { _state = _state. - remove_pending(session_name). - remove_running(session_name). - make_result(session_name, false, output_heap, process_result, - node_info = job.node_info) + remove_pending(job_name). + remove_running(job_name). + make_result(job_name, false, output_heap, process_result, node_info = job.node_info) } }