more robust command options;
authorwenzelm
Mon, 21 Aug 2023 15:54:08 +0200
changeset 78556 20360824863a
parent 78555 754bfc558d21
child 78557 131e2a220c78
more robust command options;
src/Pure/System/options.scala
src/Pure/Tools/build.scala
src/Pure/Tools/build_cluster.scala
--- a/src/Pure/System/options.scala	Mon Aug 21 15:28:35 2023 +0200
+++ b/src/Pure/System/options.scala	Mon Aug 21 15:54:08 2023 +0200
@@ -83,6 +83,8 @@
     description: String,
     section: String
   ) {
+    def spec: Spec = Spec(name, Some(value))
+
     private def print_value(x: String): String = if (typ == Options.String) quote(x) else x
     private def print_standard: String =
       standard_value match {
--- a/src/Pure/Tools/build.scala	Mon Aug 21 15:28:35 2023 +0200
+++ b/src/Pure/Tools/build.scala	Mon Aug 21 15:54:08 2023 +0200
@@ -505,6 +505,7 @@
   /* build_worker */
 
   def build_worker_command(
+    base_options: List[Options.Spec],
     host: Build_Cluster.Host,
     ssh: SSH.System = SSH.Local,
     build_id: String = "",
@@ -513,7 +514,8 @@
     dirs: List[Path] = Nil,
     verbose: Boolean = false
   ): String = {
-    val options = Options.Spec("build_hostname", Some(host.name)) :: host.options
+    val options =
+      base_options ::: Options.Spec("build_hostname", Some(host.name)) :: host.options
     ssh.bash_path(isabelle_home + Path.explode("bin/isabelle")) + " build_worker" +
       if_proper(build_id, " -B " + Bash.string(build_id)) +
       if_proper(afp_root, " -A " + ssh.bash_path(afp_root.get)) +
--- a/src/Pure/Tools/build_cluster.scala	Mon Aug 21 15:28:35 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala	Mon Aug 21 15:54:08 2023 +0200
@@ -157,7 +157,10 @@
 
     def start(): Process_Result = {
       val script =
-        Build.build_worker_command(host, ssh = ssh,
+        Build.build_worker_command(
+          List(options.check_name("build_database_server").spec),
+          host,
+          ssh = ssh,
           build_id = build_context.build_uuid,
           isabelle_home = remote_isabelle_home,
           afp_root = remote_afp_root)