diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Thu Mar 04 19:55:52 2021 +0100 +++ b/src/Pure/Tools/build.scala Thu Mar 04 21:04:27 2021 +0100 @@ -60,7 +60,7 @@ case exn: java.lang.Error => ignore_error(Exn.message(exn)) case _: XML.Error => ignore_error("") } - finally { db.close } + finally { db.close() } } } @@ -290,7 +290,7 @@ } def sleep(): Unit = - Isabelle_Thread.interrupt_handler(_ => progress.stop) { Time.seconds(0.5).sleep } + Isabelle_Thread.interrupt_handler(_ => progress.stop()) { Time.seconds(0.5).sleep } val numa_nodes = new NUMA.Nodes(numa_shuffling) @@ -306,7 +306,7 @@ if (pending.is_empty) results else { if (progress.stopped) { - for ((_, (_, job)) <- running) job.terminate + for ((_, (_, job)) <- running) job.terminate() } running.find({ case (_, (_, job)) => job.is_finished }) match {