# HG changeset patch
# User wenzelm
# Date 1709670378 -3600
# Node ID aa03d1a94e3e94754790086af566fd18cf0fcff8
# Parent  6f08aef43dc582d7bc0d64ea9dd6d8702ad12d5d
tuned signature;

diff -r 6f08aef43dc5 -r aa03d1a94e3e src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Tue Mar 05 20:58:41 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Tue Mar 05 21:26:18 2024 +0100
@@ -58,6 +58,8 @@
     start_date: Date,
     build: Option[Build_Job]
   ) extends Library.Named {
+    def cancel(): Unit = build.foreach(_.cancel())
+    def is_finished: Boolean = build.isDefined && build.get.is_finished
     def join_build: Option[Build_Job.Result] = build.flatMap(_.join)
   }
 
@@ -224,13 +226,8 @@
 
     def is_running(name: String): Boolean = running.isDefinedAt(name)
 
-    def build_running: List[Build_Job] =
-      List.from(for (job <- running.valuesIterator; build <- job.build) yield build)
-
-    def finished_running(): List[Job] =
-      List.from(
-        for (job <- running.valuesIterator; build <- job.build if build.is_finished)
-          yield job)
+    def build_running: List[Job] =
+      List.from(for (job <- running.valuesIterator if job.build.isDefined) yield job)
 
     def add_running(job: Job): State =
       copy(running = running + (job.name -> job))
@@ -1128,7 +1125,7 @@
     Isabelle_Thread.interrupt_handler(_ => progress.stop()) { build_delay.sleep() }
 
   protected def main_unsynchronized(): Unit = {
-    for (job <- _state.finished_running()) {
+    for (job <- _state.build_running.filter(_.is_finished)) {
       job.join_build match {
         case None =>
           _state = _state.remove_running(job.name)