# HG changeset patch
# User wenzelm
# Date 1692691503 -7200
# Node ID 39f6f180008d627e67eced4a80dc8fed07d6bc7b
# Parent  020fecb4da0c4afd632ab5ed1b32e742dbd20ef4
clarified signature;

diff -r 020fecb4da0c -r 39f6f180008d src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Tue Aug 22 09:39:37 2023 +0200
+++ b/src/Pure/System/options.scala	Tue Aug 22 10:05:03 2023 +0200
@@ -19,10 +19,21 @@
 
     def ISABELLE_BUILD_OPTIONS: List[Spec] =
       Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")).map(make)
+
+    def print_value(s: String): String =
+      s match {
+        case Value.Boolean(_) => s
+        case Value.Long(_) => s
+        case Value.Double(_) => s
+        case _ => Token.quote_name(specs_syntax.keywords, s)
+      }
+
+    def print(name: String, value: String): String = Properties.Eq(name, print_value(value))
   }
 
   sealed case class Spec(name: String, value: Option[String] = None, permissive: Boolean = false) {
     override def toString: String = name + if_proper(value, "=" + value.get)
+    def print: String = name + if_proper(value, "=" + Spec.print_value(value.get))
   }
 
   sealed case class Change(name: String, value: String, unknown: Boolean) {
diff -r 020fecb4da0c -r 39f6f180008d src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Aug 22 09:39:37 2023 +0200
+++ b/src/Pure/Tools/build.scala	Tue Aug 22 10:05:03 2023 +0200
@@ -520,9 +520,8 @@
       if_proper(build_id, " -B " + Bash.string(build_id)) +
       if_proper(afp_root, " -A " + ssh.bash_path(afp_root.get)) +
       dirs.map(dir => " -d " + ssh.bash_path(dir)).mkString +
-      if_proper(host.numa, " -N")
-      + " -j" + host.jobs +
-      options.map(opt => " -o " + Bash.string(Build_Cluster.Host.print_option(opt))).mkString +
+      if_proper(host.numa, " -N") + " -j" + host.jobs +
+      options.map(opt => " -o " + Bash.string(opt.print)).mkString +
       if_proper(verbose, " -v")
   }
 
diff -r 020fecb4da0c -r 39f6f180008d src/Pure/Tools/build_cluster.scala
--- a/src/Pure/Tools/build_cluster.scala	Tue Aug 22 09:39:37 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala	Tue Aug 22 10:05:03 2023 +0200
@@ -71,20 +71,6 @@
         numa = params.bool(NUMA),
         options = options)
     }
-
-    def print_name(s: String): String =
-      Token.quote_name(Options.specs_syntax.keywords, s)
-
-    def print_option(spec: Options.Spec): String = {
-      def print_value =
-        spec.value.get match {
-          case s@Value.Boolean(_) => s
-          case s@Value.Long(_) => s
-          case s@Value.Double(_) => s
-          case s => print_name(s)
-        }
-      spec.name + if_proper(spec.value, "=" + print_value)
-    }
   }
 
   class Host(
@@ -104,12 +90,12 @@
     def print: String = {
       val params =
         List(
-          if (host.user.isEmpty) "" else Properties.Eq(Host.USER, Host.print_name(host.user)),
-          if (host.port == 0) "" else Properties.Eq(Host.PORT, host.port.toString),
-          if (host.jobs == 1) "" else Properties.Eq(Host.JOBS, host.jobs.toString),
+          if (host.user.isEmpty) "" else Options.Spec.print(Host.USER, host.user),
+          if (host.port == 0) "" else Options.Spec.print(Host.PORT, host.port.toString),
+          if (host.jobs == 1) "" else Options.Spec.print(Host.JOBS, host.jobs.toString),
           if_proper(host.numa, Host.NUMA)
         ).filter(_.nonEmpty)
-      val rest = (params ::: host.options.map(Host.print_option)).mkString(",")
+      val rest = (params ::: host.options.map(_.print)).mkString(",")
 
       SSH.print_local(host.name) + if_proper(rest, ":" + rest)
     }