src/Pure/Tools/phabricator.scala
changeset 71300 ca794da3bb1d
parent 71299 51c19a44cfed
child 71301 3fdd0b93fa4b
equal deleted inserted replaced
71299:51c19a44cfed 71300:ca794da3bb1d
   847     override def toString: String = ssh_user_prefix + ssh_host + ssh_port_suffix
   847     override def toString: String = ssh_user_prefix + ssh_host + ssh_port_suffix
   848 
   848 
   849 
   849 
   850     /* execute methods */
   850     /* execute methods */
   851 
   851 
   852     def execute(
   852     def execute_raw(method: String, params: JSON.T = JSON.Object.empty): JSON.T =
   853       method: String,
   853     {
   854       args: List[String] = Nil,
   854       Isabelle_System.with_tmp_file("params", "json")(params_file =>
   855       input: JSON.T = JSON.Object.empty): JSON.T =
       
   856     {
       
   857       Isabelle_System.with_tmp_file("input", "json")(input_file =>
       
   858       {
   855       {
   859         File.write(input_file, JSON.Format(JSON.Object("params" -> JSON.Format(input))))
   856         File.write(params_file, JSON.Format(JSON.Object("params" -> JSON.Format(params))))
   860         val result =
   857         val result =
   861           Isabelle_System.bash(
   858           Isabelle_System.bash(
   862             "ssh -p " + ssh_port + " " + Bash.string(ssh_user_prefix + ssh_host) +
   859             "ssh -p " + ssh_port + " " + Bash.string(ssh_user_prefix + ssh_host) +
   863             " conduit " + Bash.strings(method :: args) + " < " + File.bash_path(input_file)).check
   860             " conduit " + Bash.string(method) + " < " + File.bash_path(params_file)).check
   864         JSON.parse(result.out, strict = false)
   861         JSON.parse(result.out, strict = false)
   865       })
   862       })
   866     }
   863     }
   867 
   864 
   868     def execute_result(
   865     def execute(method: String, params: JSON.T = JSON.Object.empty): API.Result =
   869       method: String,
   866       API.make_result(execute_raw(method, params = params))
   870       args: List[String] = Nil,
       
   871       input: JSON.T = JSON.Object.empty): API.Result =
       
   872     {
       
   873       API.make_result(execute(method, args = args, input = input))
       
   874     }
       
   875 
   867 
   876 
   868 
   877     /* concrete methods */
   869     /* concrete methods */
   878 
   870 
   879     def ping(): String = execute_result("conduit.ping").get_string
   871     def ping(): String = execute("conduit.ping").get_string
   880 
   872 
   881     lazy val user_phid: String = execute_result("user.whoami").get_value(JSON.string(_, "phid"))
   873     lazy val user_phid: String = execute("user.whoami").get_value(JSON.string(_, "phid"))
   882     lazy val user_name: String = execute_result("user.whoami").get_value(JSON.string(_, "userName"))
   874     lazy val user_name: String = execute("user.whoami").get_value(JSON.string(_, "userName"))
   883   }
   875   }
   884 
   876 
   885   object API
   877   object API
   886   {
   878   {
   887     /* result with optional error */
   879     /* result with optional error */