# HG changeset patch
# User wenzelm
# Date 1692693267 -7200
# Node ID 53e3fa5e3720f1b60c7c96708e173783546c0aa4
# Parent  c06a0396b09dc3eaa31585b704653b960e1ac8f2
clarified command-line tools;

diff -r c06a0396b09d -r 53e3fa5e3720 src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Tue Aug 22 10:31:15 2023 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Tue Aug 22 10:34:27 2023 +0200
@@ -123,6 +123,7 @@
   Build.isabelle_tool1,
   Build.isabelle_tool2,
   Build.isabelle_tool3,
+  Build.isabelle_tool4,
   CI_Build.isabelle_tool,
   Doc.isabelle_tool,
   Docker_Build.isabelle_tool,
diff -r c06a0396b09d -r 53e3fa5e3720 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Aug 22 10:31:15 2023 +0200
+++ b/src/Pure/Tools/build.scala	Tue Aug 22 10:34:27 2023 +0200
@@ -456,7 +456,7 @@
 
 
 
-  /** "isabelle build_worker" **/
+  /** build cluster management **/
 
   /* identified builds */
 
@@ -502,7 +502,54 @@
   }
 
 
-  /* build_worker */
+  /* "isabelle build_process" */
+
+  def build_process(
+    options: Options,
+    list_builds: Boolean = false,
+    progress: Progress = new Progress
+  ): Unit = {
+    val build_engine = Engine(engine_name(options))
+    val store = build_engine.build_store(options)
+
+    using(store.open_server()) { server =>
+      using_optional(store.maybe_open_build_database(server = server)) { build_database =>
+        val builds = read_builds(build_database)
+
+        if (list_builds) progress.echo(print_builds(build_database, builds))
+      }
+    }
+  }
+
+  val isabelle_tool2 = Isabelle_Tool("build_process", "manage session build process",
+    Scala_Project.here,
+    { args =>
+      var list_builds = false
+      var options =
+        Options.init(specs = Options.Spec.ISABELLE_BUILD_OPTIONS :::
+          List(Options.Spec.make("build_database")))
+
+      val getopts = Getopts("""
+Usage: isabelle build_process [OPTIONS]
+
+  Options are:
+    -l           list build processes
+    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
+""",
+        "l" -> (_ => list_builds = true),
+        "o:" -> (arg => options = options + arg))
+
+      val more_args = getopts(args)
+      if (more_args.nonEmpty) getopts.usage()
+
+      val progress = new Console_Progress()
+
+      build_process(options, list_builds = list_builds, progress = progress)
+    })
+
+
+
+  /* "isabelle build_worker" */
 
   def build_worker_command(
     host: Build_Cluster.Host,
@@ -529,12 +576,10 @@
     options: Options,
     build_id: String = "",
     progress: Progress = new Progress,
-    list_builds: Boolean = false,
     afp_root: Option[Path] = None,
     dirs: List[Path] = Nil,
     numa_shuffling: Boolean = false,
-    max_jobs: Int = 1,
-    cache: Term.Cache = Term.Cache.make()
+    max_jobs: Int = 1
   ): Option[Results] = {
     val build_engine = Engine(engine_name(options))
     val store = build_engine.build_store(options)
@@ -544,39 +589,30 @@
       using_optional(store.maybe_open_build_database(server = server)) { build_database =>
         val builds = read_builds(build_database)
 
-        if (list_builds) progress.echo(print_builds(build_database, builds))
+        val build_master = find_builds(build_database, build_id, builds)
 
-        if (!list_builds || build_id.nonEmpty) {
-          val build_master = find_builds(build_database, build_id, builds)
-
-          val sessions_structure =
-            Sessions.load_structure(build_options, dirs = AFP.make_dirs(afp_root) ::: dirs).
-              selection(Sessions.Selection(sessions = build_master.sessions))
+        val sessions_structure =
+          Sessions.load_structure(build_options, dirs = AFP.make_dirs(afp_root) ::: dirs).
+            selection(Sessions.Selection(sessions = build_master.sessions))
 
-          val build_deps =
-            Sessions.deps(sessions_structure, progress = progress, inlined_files = true).check_errors
+        val build_deps =
+          Sessions.deps(sessions_structure, progress = progress, inlined_files = true).check_errors
 
-          val build_context =
-            Context(store, build_engine, build_deps, afp_root = afp_root,
-              hostname = hostname(build_options), numa_shuffling = numa_shuffling,
-              max_jobs = max_jobs, build_uuid = build_master.build_uuid)
+        val build_context =
+          Context(store, build_engine, build_deps, afp_root = afp_root,
+            hostname = hostname(build_options), numa_shuffling = numa_shuffling,
+            max_jobs = max_jobs, build_uuid = build_master.build_uuid)
 
-          Some(build_engine.run_build_process(build_context, progress, server))
-        }
-        else None
+        Some(build_engine.run_build_process(build_context, progress, server))
       }
     }
   }
 
-
-  /* command-line wrapper */
-
-  val isabelle_tool2 = Isabelle_Tool("build_worker", "external worker for session build process",
+  val isabelle_tool3 = Isabelle_Tool("build_worker", "start worker for session build process",
     Scala_Project.here,
     { args =>
       var afp_root: Option[Path] = None
       var build_id = ""
-      var list_builds = false
       var numa_shuffling = false
       val dirs = new mutable.ListBuffer[Path]
       var max_jobs = 1
@@ -594,7 +630,6 @@
     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
     -d DIR       include session directory
     -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
 """,
@@ -603,7 +638,6 @@
         "N" -> (_ => numa_shuffling = true),
         "d:" -> (arg => dirs += Path.explode(arg)),
         "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
-        "l" -> (_ => list_builds = true),
         "o:" -> (arg => options = options + arg),
         "v" -> (_ => verbose = true))
 
@@ -617,7 +651,6 @@
           build_worker(options,
             build_id = build_id,
             progress = progress,
-            list_builds = list_builds,
             afp_root = afp_root,
             dirs = dirs.toList,
             numa_shuffling = Host.numa_check(progress, numa_shuffling),
@@ -802,7 +835,7 @@
 
   /* command-line wrapper */
 
-  val isabelle_tool3 = Isabelle_Tool("build_log", "print messages from session build database",
+  val isabelle_tool4 = Isabelle_Tool("build_log", "print messages from session build database",
     Scala_Project.here,
     { args =>
       /* arguments */