# HG changeset patch
# User wenzelm
# Date 1689937327 -7200
# Node ID 0be7e94fd24371fbc85e13ef2ccaf685fd35dcfa
# Parent  62d7ef1da4411b81d0b0c1cafb0f7f864b2b99e7
more accurate print vs. parse;

diff -r 62d7ef1da441 -r 0be7e94fd243 src/Pure/Tools/build_cluster.scala
--- a/src/Pure/Tools/build_cluster.scala	Fri Jul 21 11:31:33 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala	Fri Jul 21 13:02:07 2023 +0200
@@ -67,6 +67,20 @@
         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)
+    }
   }
 
   final class Host private(
@@ -84,12 +98,12 @@
     def print: String = {
       val params =
         List(
-          if (user.isEmpty) "" else Properties.Eq(Host.USER, user),
+          if (user.isEmpty) "" else Properties.Eq(Host.USER, Host.print_name(user)),
           if (port == 0) "" else Properties.Eq(Host.PORT, port.toString),
           if (jobs == 1) "" else Properties.Eq(Host.JOBS, jobs.toString),
           if_proper(numa, Host.NUMA)
         ).filter(_.nonEmpty)
-      val rest = (params ::: options).mkString(",")
+      val rest = (params ::: options.map(Host.print_option)).mkString(",")
 
       SSH.print_local(name) + if_proper(rest, ":" + rest)
     }