# HG changeset patch
# User wenzelm
# Date 1576613986 -3600
# Node ID ca794da3bb1d61c5987ad7f1e564780a19188e8d
# Parent  51c19a44cfedc8c24042545769bd7d5444d9af13
tuned signature;

diff -r 51c19a44cfed -r ca794da3bb1d src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Tue Dec 17 21:04:55 2019 +0100
+++ b/src/Pure/Tools/phabricator.scala	Tue Dec 17 21:19:46 2019 +0100
@@ -849,37 +849,29 @@
 
     /* execute methods */
 
-    def execute(
-      method: String,
-      args: List[String] = Nil,
-      input: JSON.T = JSON.Object.empty): JSON.T =
+    def execute_raw(method: String, params: JSON.T = JSON.Object.empty): JSON.T =
     {
-      Isabelle_System.with_tmp_file("input", "json")(input_file =>
+      Isabelle_System.with_tmp_file("params", "json")(params_file =>
       {
-        File.write(input_file, JSON.Format(JSON.Object("params" -> JSON.Format(input))))
+        File.write(params_file, JSON.Format(JSON.Object("params" -> JSON.Format(params))))
         val result =
           Isabelle_System.bash(
             "ssh -p " + ssh_port + " " + Bash.string(ssh_user_prefix + ssh_host) +
-            " conduit " + Bash.strings(method :: args) + " < " + File.bash_path(input_file)).check
+            " conduit " + Bash.string(method) + " < " + File.bash_path(params_file)).check
         JSON.parse(result.out, strict = false)
       })
     }
 
-    def execute_result(
-      method: String,
-      args: List[String] = Nil,
-      input: JSON.T = JSON.Object.empty): API.Result =
-    {
-      API.make_result(execute(method, args = args, input = input))
-    }
+    def execute(method: String, params: JSON.T = JSON.Object.empty): API.Result =
+      API.make_result(execute_raw(method, params = params))
 
 
     /* concrete methods */
 
-    def ping(): String = execute_result("conduit.ping").get_string
+    def ping(): String = execute("conduit.ping").get_string
 
-    lazy val user_phid: String = execute_result("user.whoami").get_value(JSON.string(_, "phid"))
-    lazy val user_name: String = execute_result("user.whoami").get_value(JSON.string(_, "userName"))
+    lazy val user_phid: String = execute("user.whoami").get_value(JSON.string(_, "phid"))
+    lazy val user_name: String = execute("user.whoami").get_value(JSON.string(_, "userName"))
   }
 
   object API