--- 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) {
--- 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")
}
--- 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)
}