clarified signature: separate unrelated modules;
authorwenzelm
Tue, 13 Sep 2022 09:38:02 +0200
changeset 76129 5979f73b9db1
parent 76128 f5e96a4039a7
child 76130 b703cecf9bd0
clarified signature: separate unrelated modules;
src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Tue Sep 13 09:24:31 2022 +0200
+++ b/src/Pure/Tools/phabricator.scala	Tue Sep 13 09:38:02 2022 +0200
@@ -64,7 +64,7 @@
 
   val default_mailers: Path = Path.explode("mailers.json")
 
-  val default_system_port: Int = SSH.default_port
+  val default_system_port: Int = 22
   val alternative_system_port = 222
   val default_server_port = 2222
 
@@ -663,14 +663,14 @@
   private val Any_Port = """^#?\s*Port\b.*$""".r
 
   def conf_ssh_port(port: Int): String =
-    if (port == SSH.default_port) "#Port " + SSH.default_port else "Port " + port
+    if (port == default_system_port) "#Port " + default_system_port else "Port " + port
 
   def read_ssh_port(conf: Path): Int = {
     val lines = split_lines(File.read(conf))
     val ports =
       lines.flatMap({
         case Port(Value.Int(p)) => Some(p)
-        case No_Port() => Some(SSH.default_port)
+        case No_Port() => Some(default_system_port)
         case _ => None
       })
     ports match {
@@ -774,7 +774,7 @@
     for (config <- configs) {
       progress.echo("phabricator " + quote(config.name) + " port " +  server_port)
       config.execute("config set diffusion.ssh-port " + Bash.string(server_port.toString))
-      if (server_port == SSH.default_port) config.execute("config delete diffusion.ssh-port")
+      if (server_port == default_system_port) config.execute("config delete diffusion.ssh-port")
     }
   }
 
@@ -889,7 +889,7 @@
 
     /* context for operations */
 
-    def apply(user: String, host: String, port: Int = SSH.default_port): API =
+    def apply(user: String, host: String, port: Int = default_system_port): API =
       new API(user, host, port)
   }
 
@@ -898,8 +898,11 @@
 
     require(ssh_host.nonEmpty && ssh_port >= 0, "bad ssh host or port")
 
-    private def ssh_user_prefix: String = SSH.user_prefix(ssh_user)
-    private def ssh_port_suffix: String = SSH.port_suffix(ssh_port)
+    private def ssh_user_prefix: String =
+      if (ssh_user.nonEmpty) ssh_user + "@" else ""
+
+    private def ssh_port_suffix: String =
+      if (ssh_port != default_system_port) ":" + ssh_port else ""
 
     override def toString: String = ssh_user_prefix + ssh_host + ssh_port_suffix
     def hg_url: String = "ssh://" + ssh_user_prefix + ssh_host + ssh_port_suffix