# HG changeset patch
# User wenzelm
# Date 1678271206 -3600
# Node ID 149d48a4801b330ea9ef6fb4182fee228ce7fe5c
# Parent  f78286d2e30f1769e8daa023144f0e150da80eae
support for "isabelle build -j0": require external workers to make progress;

diff -r f78286d2e30f -r 149d48a4801b src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Mar 08 10:47:32 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Mar 08 11:26:46 2023 +0100
@@ -141,6 +141,8 @@
     def store_heap(name: String): Boolean =
       build_heap || Sessions.is_pure(name) ||
       sessions.valuesIterator.exists(_.ancestors.contains(name))
+
+    def worker: Boolean = max_jobs > 1
   }
 
 
@@ -796,7 +798,7 @@
   }
 
   protected def next_job(state: Build_Process.State): Option[String] =
-    if (state.running.size < (build_context.max_jobs max 1)) {
+    if (progress.stopped || state.running.size < build_context.max_jobs) {
       state.pending.filter(entry => entry.is_ready && !state.is_running(entry.name))
         .sortBy(_.name)(build_context.ordering)
         .headOption.map(_.name)
@@ -835,7 +837,7 @@
         remove_pending(session_name).
         make_result(session_name, Process_Result.error, output_shasum)
     }
-    else if (!ancestor_results.forall(_.ok) || progress.stopped) {
+    else if (progress.stopped || !ancestor_results.forall(_.ok)) {
       progress.echo(session_name + " CANCELLED")
       state
         .remove_pending(session_name)
@@ -916,7 +918,10 @@
     }
     else {
       if (master) start_build()
-      start_worker()
+
+      val worker = build_context.worker
+      if (worker) start_worker() else progress.echo("Waiting for external workers ...")
+
       try {
         while (!finished()) {
           if (progress.stopped) synchronized_database { _state.stop_running() }
@@ -939,7 +944,7 @@
         }
       }
       finally {
-        stop_worker()
+        if (worker) stop_worker()
         if (master) stop_build()
       }