--- a/src/Pure/Build/build_process.scala Mon Mar 04 12:30:33 2024 +0100
+++ b/src/Pure/Build/build_process.scala Mon Mar 04 13:44:11 2024 +0100
@@ -1118,13 +1118,16 @@
/* run */
+ protected def finished_unsynchronized(): Boolean =
+ if (!build_context.master && progress.stopped) _state.build_running.isEmpty
+ else _state.pending.isEmpty
+
+ protected def sleep(): Unit =
+ Isabelle_Thread.interrupt_handler(_ => progress.stop()) { build_delay.sleep() }
+
def run(): Build.Results = {
var finished = false
- def finished_unsynchronized(): Boolean =
- if (!build_context.master && progress.stopped) _state.build_running.isEmpty
- else _state.pending.isEmpty
-
synchronized_database("Build_Process.init") {
if (build_context.master) {
_build_cluster.init()
@@ -1134,9 +1137,6 @@
finished = finished_unsynchronized()
}
- def sleep(): Unit =
- Isabelle_Thread.interrupt_handler(_ => progress.stop()) { build_delay.sleep() }
-
val build_progress_warnings = Synchronized(Set.empty[String])
def build_progress_warning(msg: String): Unit =
build_progress_warnings.change(seen =>