# HG changeset patch
# User wenzelm
# Date 1689516758 -7200
# Node ID 6689b4c07bba7c74c91b0b71bd7d2575ad54612e
# Parent  4978a158dc4c277166b6c703d2aac94051381be5
clarified signature: proper Scala function for command-line tool;

diff -r 4978a158dc4c -r 6689b4c07bba src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Jul 16 16:11:12 2023 +0200
+++ b/src/Pure/Tools/build.scala	Sun Jul 16 16:12:38 2023 +0200
@@ -392,40 +392,45 @@
 
   /* identified builds */
 
-  def read_builds(options: Options): List[Build_Process.Build] =
-    using_option(Store(options).maybe_open_build_database())(
-      Build_Process.read_builds).getOrElse(Nil).filter(_.active)
-
-  def print_builds(options: Options, builds: List[Build_Process.Build]): String =
-    using_optional(Store(options).maybe_open_build_database()) { build_database =>
-      val print_database =
-        build_database match {
-          case None => ""
-          case Some(db) => " (database: " + db + ")"
-        }
-      if (builds.isEmpty) "No build processes available" + print_database
-      else {
-        "Available build processes" + print_database +
-          (for ((build, i) <- builds.iterator.zipWithIndex)
-            yield {
-              "\n  " + (i + 1) + ": " + build.build_uuid +
-                " (platform: " + build.ml_platform +
-                ", start: " + Build_Log.print_date(build.start) + ")"
-            }).mkString
-      }
+  def read_builds(build_database: Option[SQL.Database]): List[Build_Process.Build] =
+    build_database match {
+      case None => Nil
+      case Some(db) => Build_Process.read_builds(db).filter(_.active)
     }
 
+  def print_builds(build_database: Option[SQL.Database], builds: List[Build_Process.Build]): String =
+  {
+    val print_database =
+      build_database match {
+        case None => ""
+        case Some(db) => " (database: " + db + ")"
+      }
+    if (builds.isEmpty) "No build processes available" + print_database
+    else {
+      "Available build processes" + print_database +
+        (for ((build, i) <- builds.iterator.zipWithIndex)
+          yield {
+            "\n  " + (i + 1) + ": " + build.build_uuid +
+              " (platform: " + build.ml_platform +
+              ", start: " + Build_Log.print_date(build.start) + ")"
+          }).mkString
+    }
+  }
+
   def id_builds(
-    options: Options,
-    id: String,
+    build_database: Option[SQL.Database],
+    build_id: String,
     builds: List[Build_Process.Build]
   ): Build_Process.Build =
-    (id, builds.length) match {
+    (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 == id) => builds.find(_.build_uuid == id).get
-      case ("", 0) => error(print_builds(options, builds))
+      case (UUID(_), _) if builds.exists(_.build_uuid == build_id) =>
+        builds.find(_.build_uuid == build_id).get
+      case ("", 0) => error(print_builds(build_database, builds))
       case ("", 1) => builds.head
-      case _ => cat_error("Cannot identify build process " + quote(id), print_builds(options, builds))
+      case _ =>
+        cat_error("Cannot identify build process " + quote(build_id),
+          print_builds(build_database, builds))
     }
 
 
@@ -433,30 +438,42 @@
 
   def build_worker(
     options: Options,
-    build_master: Build_Process.Build,
+    build_id: String,
     progress: Progress = new Progress,
+    list_builds: Boolean = false,
     dirs: List[Path] = Nil,
     numa_shuffling: Boolean = false,
     max_jobs: Int = 1,
     cache: Term.Cache = Term.Cache.make()
-  ): Results = {
+  ): Option[Results] = {
     val build_engine = Engine(engine_name(options))
-
-    val store = build_engine.build_store(options, cache = cache)
+    val store = build_engine.build_store(options)
     val build_options = store.options
 
-    val sessions_structure =
-      Sessions.load_structure(build_options, dirs = dirs).
-        selection(Sessions.Selection(sessions = build_master.sessions))
+    using_optional(store.maybe_open_build_database()) { build_database =>
+      val builds = read_builds(build_database)
+
+      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 sessions_structure =
+          Sessions.load_structure(build_options, dirs = 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 =
-      Build_Process.Context(store, build_deps, hostname = hostname(build_options),
-        numa_shuffling = numa_shuffling, max_jobs = max_jobs, build_uuid = build_master.build_uuid)
+        val build_context =
+          Build_Process.Context(store, build_deps, hostname = hostname(build_options),
+            numa_shuffling = numa_shuffling, max_jobs = max_jobs,
+            build_uuid = build_master.build_uuid)
 
-    build_engine.run(build_context, progress)
+        Some(build_engine.run(build_context, progress))
+      }
+      else None
+    }
   }
 
 
@@ -504,23 +521,19 @@
 
       val progress = new Console_Progress(verbose = verbose)
 
-      val builds = read_builds(options)
-
-      if (list_builds) progress.echo(print_builds(options, builds))
-
-      if (!list_builds || build_id.nonEmpty) {
-        val build = id_builds(options, build_id, builds)
+      val res =
+        progress.interrupt_handler {
+          build_worker(options, build_id,
+            progress = progress,
+            list_builds = list_builds,
+            dirs = dirs,
+            numa_shuffling = Host.numa_check(progress, numa_shuffling),
+            max_jobs = max_jobs)
+        }
 
-        val results =
-          progress.interrupt_handler {
-            build_worker(options, build,
-              progress = progress,
-              dirs = dirs,
-              numa_shuffling = Host.numa_check(progress, numa_shuffling),
-              max_jobs = max_jobs)
-          }
-
-        sys.exit(results.rc)
+      res match {
+        case Some(results) if !results.ok => sys.exit(results.rc)
+        case _ =>
       }
     })