# HG changeset patch
# User wenzelm
# Date 1689778102 -7200
# Node ID c5170293d392ebf4a85156d81aacd6339cd261a4
# Parent  f2d67c78b6897af0f9e6436004da05cb569a3e09
clarified options;

diff -r f2d67c78b689 -r c5170293d392 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Jul 19 16:04:59 2023 +0200
+++ b/src/Pure/Tools/build.scala	Wed Jul 19 16:48:22 2023 +0200
@@ -435,35 +435,36 @@
       "Available build processes" + print_database +
         (for ((build, i) <- builds.iterator.zipWithIndex)
           yield {
-            "\n  " + (i + 1) + ": " + build.build_uuid +
+            "\n  " + build.build_uuid +
               " (platform: " + build.ml_platform +
               ", start: " + Build_Log.print_date(build.start) + ")"
           }).mkString
     }
   }
 
-  def id_builds(
+  def find_builds(
     build_database: Option[SQL.Database],
     build_id: String,
     builds: List[Build_Process.Build]
-  ): Build_Process.Build =
+  ): Build_Process.Build = {
     (build_id, builds.length) match {
-      case (Value.Int(i), n) if 1 <= i && i <= n => builds(i - 1)
       case (UUID(_), _) if builds.exists(_.build_uuid == build_id) =>
         builds.find(_.build_uuid == build_id).get
+      case ("", 1) => builds.head
       case ("", 0) => error(print_builds(build_database, builds))
-      case ("", 1) => builds.head
       case _ =>
         cat_error("Cannot identify build process " + quote(build_id),
           print_builds(build_database, builds))
     }
+  }
 
 
   /* build_worker */
 
   def build_worker(
     options: Options,
-    build_id: String,
+    build_id: String = "",
+    worker_id: String = "",
     progress: Progress = new Progress,
     list_builds: Boolean = false,
     dirs: List[Path] = Nil,
@@ -482,7 +483,7 @@
         if (list_builds) progress.echo(print_builds(build_database, builds))
 
         if (!list_builds || build_id.nonEmpty) {
-          val build_master = id_builds(build_database, build_id, builds)
+          val build_master = find_builds(build_database, build_id, builds)
 
           val sessions_structure =
             Sessions.load_structure(build_options, dirs = dirs).
@@ -523,21 +524,17 @@
 Usage: isabelle build_worker [OPTIONS]
 
   Options are:
+    -B UUID      identify build process: mandatory for multiple active builds
     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
     -d DIR       include session directory
-    -i ID        identify build process, either via index (starting from 1) or
-                 Universally Unique Identifier (UUID)
     -j INT       maximum number of parallel jobs (default 1)
     -l           list build processes
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -v           verbose
-
-  Run as external worker for session build process, as identified via
-  option -i. The latter can be omitted, if there is exactly one build.
 """,
+        "B:" -> (arg => build_id = arg),
         "N" -> (_ => numa_shuffling = true),
         "d:" -> (arg => dirs += Path.explode(arg)),
-        "i:" -> (arg => build_id = arg),
         "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
         "l" -> (_ => list_builds = true),
         "o:" -> (arg => options = options + arg),