# HG changeset patch
# User wenzelm
# Date 1689931893 -7200
# Node ID 62d7ef1da4411b81d0b0c1cafb0f7f864b2b99e7
# Parent  e5908be41a36931fab676a01ca63dff6e339340f
clarified signature;
tuned output;

diff -r e5908be41a36 -r 62d7ef1da441 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Fri Jul 21 11:21:43 2023 +0200
+++ b/src/Pure/General/ssh.scala	Fri Jul 21 11:31:33 2023 +0200
@@ -80,6 +80,15 @@
   }
 
 
+  /* local host (not "localhost") */
+
+  val LOCAL = "local"
+
+  def is_local(host: String): Boolean = host.isEmpty || host == LOCAL
+
+  def print_local(host: String): String = if (is_local(host)) LOCAL else host
+
+
   /* open session */
 
   def open_session(
@@ -88,6 +97,8 @@
     port: Int = 0,
     user: String = ""
   ): Session = {
+    require(!is_local(host), "Illegal host name " + quote(host))
+
     val multiplex = options.bool("ssh_multiplexing") && !Platform.is_windows
     val (control_master, control_path) =
       if (multiplex) (true, Isabelle_System.tmp_file("ssh", initialized = false).getPath)
@@ -431,7 +442,7 @@
 
     def close(): Unit = ()
 
-    override def toString: String = "SSH.Local"
+    override def toString: String = LOCAL
     def print: String = ""
     def hg_url: String = ""
     def client_command: String = ""
diff -r e5908be41a36 -r 62d7ef1da441 src/Pure/Tools/build_cluster.scala
--- a/src/Pure/Tools/build_cluster.scala	Fri Jul 21 11:21:43 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala	Fri Jul 21 11:31:33 2023 +0200
@@ -12,8 +12,6 @@
   /* host specifications */
 
   object Host {
-    val LOCAL = "local"
-
     private val rfc822_specials = """()<>@,;:\"[]"""
 
     private val USER = "user"
@@ -79,7 +77,7 @@
     numa: Boolean,
     options: List[Options.Spec]
   ) {
-    def is_local: Boolean = name.isEmpty || name == Host.LOCAL
+    def is_local: Boolean = SSH.is_local(name)
 
     override def toString: String = print
 
@@ -93,7 +91,7 @@
         ).filter(_.nonEmpty)
       val rest = (params ::: options).mkString(",")
 
-      (if (is_local) Host.LOCAL else name) + if_proper(rest, ":" + rest)
+      SSH.print_local(name) + if_proper(rest, ":" + rest)
     }
 
     def open_ssh_session(options: Options): SSH.Session =