# HG changeset patch
# User wenzelm
# Date 1709556251 -3600
# Node ID 8fa5b82a6964249c401757467a4cddd3181baf3c
# Parent  de611b17762c054649c5bf76a5b27c152e2c5650
tuned signature: more protected operations;

diff -r de611b17762c -r 8fa5b82a6964 src/Pure/Build/build_process.scala
--- 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 =>