diff -r 93b097726667 -r 51c19a44cfed src/Pure/Tools/phabricator.scala --- a/src/Pure/Tools/phabricator.scala Tue Dec 17 20:34:47 2019 +0100 +++ b/src/Pure/Tools/phabricator.scala Tue Dec 17 21:04:55 2019 +0100 @@ -124,7 +124,7 @@ - /** command-line tools **/ + /** administrative tools **/ /* Isabelle tool wrapper */ @@ -824,4 +824,152 @@ phabricator_setup_ssh( server_port = server_port, system_port = system_port, progress = progress) }) + + + + /** conduit API **/ + + object Conduit + { + def apply(ssh_host: String, ssh_user: String, ssh_port: Int = 22): Conduit = + new Conduit(ssh_host, ssh_user, ssh_port) + } + + final class Conduit private(ssh_host: String, ssh_user: String, ssh_port: Int) + { + /* connection */ + + require(ssh_host.nonEmpty && ssh_port >= 0) + + private def ssh_user_prefix: String = if (ssh_user.isEmpty) "" else ssh_user + "@" + private def ssh_port_suffix: String = if (ssh_port == 22) "" else ":" + ssh_port + + override def toString: String = ssh_user_prefix + ssh_host + ssh_port_suffix + + + /* execute methods */ + + def execute( + method: String, + args: List[String] = Nil, + input: JSON.T = JSON.Object.empty): JSON.T = + { + Isabelle_System.with_tmp_file("input", "json")(input_file => + { + File.write(input_file, JSON.Format(JSON.Object("params" -> JSON.Format(input)))) + 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 + 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)) + } + + + /* concrete methods */ + + def ping(): String = execute_result("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")) + } + + object API + { + /* result with optional error */ + + object Error_Code extends Enumeration + { + val bad_diff = Value("ERR-BAD-DIFF") + val bad_document = Value("ERR-BAD-DOCUMENT") + val bad_file = Value("ERR-BAD-FILE") + val bad_phid = Value("ERR-BAD-PHID") + val bad_revision = Value("ERR-BAD-REVISION") + val bad_task = Value("ERR-BAD-TASK") + val bad_token = Value("ERR-BAD-TOKEN") + val bad_version = Value("ERR-BAD-VERSION") + val conduit_call = Value("ERR-CONDUIT-CALL") + val conduit_core = Value("ERR-CONDUIT-CORE") + val invalid_auth = Value("ERR-INVALID-AUTH") + val invalid_certificate = Value("ERR-INVALID-CERTIFICATE") + val invalid_engine_ = Value("ERR-INVALID_ENGINE") // FIXME !? + val invalid_engine = Value("ERR-INVALID-ENGINE") + val invalid_parameter = Value("ERR-INVALID-PARAMETER") + val invalid_session = Value("ERR-INVALID-SESSION") + val invalid_token = Value("ERR-INVALID-TOKEN") + val invalid_usage = Value("ERR-INVALID-USAGE") + val invalid_user = Value("ERR-INVALID-USER") + val need_diff = Value("ERR-NEED-DIFF") + val need_file = Value("ERR-NEED-FILE") + val no_certificate = Value("ERR-NO-CERTIFICATE") + val no_content = Value("ERR-NO-CONTENT") + val no_effect = Value("ERR-NO-EFFECT") + val no_paste = Value("ERR-NO-PASTE") + val not_found = Value("ERR-NOT-FOUND") + val not_pusher = Value("ERR-NOT-PUSHER") + val oauth_access = Value("ERR-OAUTH-ACCESS") + val permissions = Value("ERR-PERMISSIONS") + val rate_limit = Value("ERR-RATE-LIMIT") + val unknown_client = Value("ERR-UNKNOWN-CLIENT") + val unknown_repository = Value("ERR-UNKNOWN-REPOSITORY") + val unknown_type = Value("ERR-UNKNOWN-TYPE") + val unknown_vcs_type = Value("ERR-UNKNOWN-VCS-TYPE") + val unsupported_vcs = Value("ERR-UNSUPPORTED-VCS") + + val unknown_error = Value("ERR-UNKNOWN-ERROR") + } + + sealed case class Result( + result: JSON.T, + error_code: Option[Error_Code.Value], + error_info: String) + { + def ok: Boolean = error_code.isEmpty && error_info.isEmpty + + def get: JSON.T = + if (error_info.nonEmpty) error(error_info) + else if (error_code.nonEmpty) error(error_code.get.toString) + else result + + def get_value[A](unapply: JSON.T => Option[A]): A = + unapply(get) getOrElse error("Bad JSON result: " + JSON.Format(result)) + + def get_string: String = get_value(JSON.Value.String.unapply) + } + + def make_error_code(str: String): Error_Code.Value = + try { Error_Code.withName(str) } + catch { case _: java.util.NoSuchElementException => Error_Code.unknown_error } + + def make_result(json: JSON.T): Result = + Result( + JSON.value(json, "result").getOrElse(JSON.Object.empty), + JSON.string(json, "error_code").map(make_error_code), + JSON.string(json, "error_info").getOrElse("")) + + + /* repository operations */ + + object VCS extends Enumeration + { + val hg, git, svn = Value + } + + def edit(typ: String, value: JSON.T): JSON.Object.T = + JSON.Object("type" -> typ, "value" -> value) + + def edits(typ: String, value: Option[JSON.T]): List[JSON.Object.T] = + List(edit(typ, value)) + + def opt_edits(typ: String, value: Option[JSON.T]): List[JSON.Object.T] = + value.map(edit(typ, _)).toList + } }