# HG changeset patch
# User wenzelm
# Date 1663333550 -7200
# Node ID 81241a1d3d993cb9ddd82cb176c918c864037c04
# Parent  f740d62a3470d38ffbcc017f78536f2f82038494
tuned signature;

diff -r f740d62a3470 -r 81241a1d3d99 src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Fri Sep 16 15:03:08 2022 +0200
+++ b/src/Pure/Tools/phabricator.scala	Fri Sep 16 15:05:50 2022 +0200
@@ -889,18 +889,16 @@
 
     /* context for operations */
 
-    def apply(ssh_target: String, ssh_port: Int = default_system_port): API =
-      new API(ssh_target, ssh_port)
+    def apply(server: String, port: Int = default_system_port): API =
+      new API(server, port)
   }
 
-  final class API private(ssh_target: String, ssh_port: Int) {
+  final class API private(server: String, port: Int) {
     /* connection */
 
-    private def ssh_port_suffix: String =
-      if (ssh_port > 0) ":" + ssh_port else ""
-
-    override def toString: String = ssh_target + ssh_port_suffix
-    def hg_url: String = "ssh://" + ssh_target + ssh_port_suffix
+    private def port_suffix: String = if (port > 0) ":" + port else ""
+    override def toString: String = server + port_suffix
+    def hg_url: String = "ssh://" + server + port_suffix
 
 
     /* execute methods */
@@ -910,7 +908,7 @@
         File.write(params_file, JSON.Format(JSON.Object("params" -> JSON.Format(params))))
         val result =
           Isabelle_System.bash(
-            SSH.client_command(port = ssh_port) + " -- " + Bash.string(ssh_target) +
+            SSH.client_command(port = port) + " -- " + Bash.string(server) +
             " conduit " + Bash.string(method) + " < " + File.bash_path(params_file)).check
         JSON.parse(result.out, strict = false)
       }