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 */ |