tuned signature: more protected operations;
authorwenzelm
Mon, 04 Mar 2024 13:44:11 +0100
changeset 79763 8fa5b82a6964
parent 79762 de611b17762c
child 79764 5857bb16cf30
tuned signature: more protected operations;
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 =>