--- a/src/Pure/Admin/build_release.scala Fri Sep 16 14:02:02 2022 +0200
+++ b/src/Pure/Admin/build_release.scala Fri Sep 16 14:26:42 2022 +0200
@@ -231,14 +231,10 @@
" (" + server_option + " = " + quote(server) + ") ...")
val ssh =
- server match {
- case "" =>
- if (Platform.family == platform) SSH.Local
- else error("Undefined option " + server_option + ": cannot build heaps")
- case SSH.Target(user, host) =>
- SSH.open_session(options, host = host, user = user)
- case _ => error("Malformed option " + server_option + ": " + quote(server))
- }
+ if (server.nonEmpty) SSH.open_session(options, server)
+ else if (Platform.family == platform) SSH.Local
+ else error("Undefined option " + server_option + ": cannot build heaps")
+
try {
Isabelle_System.with_tmp_file("tmp", ext = "tar") { local_tmp_tar =>
execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .")
--- a/src/Pure/General/mercurial.scala Fri Sep 16 14:02:02 2022 +0200
+++ b/src/Pure/General/mercurial.scala Fri Sep 16 14:26:42 2022 +0200
@@ -467,40 +467,38 @@
/* remote repository */
- val remote_url =
- remote match {
- case _ if remote.startsWith("ssh://") =>
- val ssh_url = remote + "/" + repos_name
+ val remote_url = {
+ if (remote.startsWith("ssh://")) {
+ val ssh_url = remote + "/" + repos_name
+
+ if (!remote_exists) {
+ try { local_hg.command("init", ssh_url, repository = false).check }
+ catch { case ERROR(msg) => progress.echo_warning(msg) }
+ }
- if (!remote_exists) {
- try { local_hg.command("init", ssh_url, repository = false).check }
- catch { case ERROR(msg) => progress.echo_warning(msg) }
+ ssh_url
+ }
+ else {
+ val phabricator = Phabricator.API(remote)
+
+ var repos =
+ phabricator.get_repositories().find(r => r.short_name == repos_name) getOrElse {
+ if (remote_exists) {
+ error("Remote repository " +
+ quote(phabricator.hg_url + "/source/" + repos_name) + " expected to exist")
+ }
+ else phabricator.create_repository(repos_name, short_name = repos_name)
}
- ssh_url
-
- case SSH.Target(user, host) =>
- val phabricator = Phabricator.API(user, host)
+ while (repos.importing) {
+ progress.echo("Awaiting remote repository ...")
+ Time.seconds(0.5).sleep()
+ repos = phabricator.the_repository(repos.phid)
+ }
- var repos =
- phabricator.get_repositories().find(r => r.short_name == repos_name) getOrElse {
- if (remote_exists) {
- error("Remote repository " +
- quote(phabricator.hg_url + "/source/" + repos_name) + " expected to exist")
- }
- else phabricator.create_repository(repos_name, short_name = repos_name)
- }
-
- while (repos.importing) {
- progress.echo("Awaiting remote repository ...")
- Time.seconds(0.5).sleep()
- repos = phabricator.the_repository(repos.phid)
- }
-
- repos.ssh_url
-
- case _ => error("Malformed remote specification " + quote(remote))
+ repos.ssh_url
}
+ }
progress.echo("Remote repository " + quote(remote_url))
--- a/src/Pure/General/ssh.scala Fri Sep 16 14:02:02 2022 +0200
+++ b/src/Pure/General/ssh.scala Fri Sep 16 14:26:42 2022 +0200
@@ -13,22 +13,6 @@
object SSH {
- /* target machine: user@host syntax */
-
- object Target {
- def parse(s: String): (String, String) = {
- val i = s.indexOf('@')
- if (i <= 0) ("", s)
- else (s.substring(0, i), s.substring(i + 1))
- }
-
- def unapplySeq(s: String): Option[List[String]] = {
- val (user, host) = parse(s)
- if (host.isEmpty) None else Some(List(user, host))
- }
- }
-
-
/* OpenSSH configuration and command-line */
// see https://linux.die.net/man/5/ssh_config
--- a/src/Pure/System/components.scala Fri Sep 16 14:02:02 2022 +0200
+++ b/src/Pure/System/components.scala Fri Sep 16 14:26:42 2022 +0200
@@ -221,68 +221,67 @@
}
if ((publish && archives.nonEmpty) || update_components_sha1) {
- options.string("isabelle_components_server") match {
- case SSH.Target(user, host) =>
- using(SSH.open_session(options, host = host, user = user)) { ssh =>
- val components_dir = Path.explode(options.string("isabelle_components_dir"))
- val contrib_dir = Path.explode(options.string("isabelle_components_contrib_dir"))
+ val server = options.string("isabelle_components_server")
+ if (server.isEmpty) error("Undefined option isabelle_components_server")
- for (dir <- List(components_dir, contrib_dir) if !ssh.is_dir(dir)) {
- error("Bad remote directory: " + dir)
- }
+ using(SSH.open_session(options, server)) { ssh =>
+ val components_dir = Path.explode(options.string("isabelle_components_dir"))
+ val contrib_dir = Path.explode(options.string("isabelle_components_contrib_dir"))
- if (publish) {
- for (archive <- archives) {
- val archive_name = archive.file_name
- val name = Archive.get_name(archive_name)
- val remote_component = components_dir + archive.base
- val remote_contrib = contrib_dir + Path.explode(name)
+ for (dir <- List(components_dir, contrib_dir) if !ssh.is_dir(dir)) {
+ error("Bad remote directory: " + dir)
+ }
- // component archive
- if (ssh.is_file(remote_component) && !force) {
- error("Remote component archive already exists: " + remote_component)
- }
- progress.echo("Uploading " + archive_name)
- ssh.write_file(remote_component, archive)
+ if (publish) {
+ for (archive <- archives) {
+ val archive_name = archive.file_name
+ val name = Archive.get_name(archive_name)
+ val remote_component = components_dir + archive.base
+ val remote_contrib = contrib_dir + Path.explode(name)
- // contrib directory
- val is_standard_component =
- Isabelle_System.with_tmp_dir("component") { tmp_dir =>
- Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
- check_dir(tmp_dir + Path.explode(name))
- }
- if (is_standard_component) {
- if (ssh.is_dir(remote_contrib)) {
- if (force) ssh.rm_tree(remote_contrib)
- else error("Remote component directory already exists: " + remote_contrib)
- }
- progress.echo("Unpacking remote " + archive_name)
- ssh.execute("tar -C " + ssh.bash_path(contrib_dir) + " -xzf " +
- ssh.bash_path(remote_component)).check
- }
- else {
- progress.echo_warning("No unpacking of non-standard component: " + archive_name)
- }
+ // component archive
+ if (ssh.is_file(remote_component) && !force) {
+ error("Remote component archive already exists: " + remote_component)
+ }
+ progress.echo("Uploading " + archive_name)
+ ssh.write_file(remote_component, archive)
+
+ // contrib directory
+ val is_standard_component =
+ Isabelle_System.with_tmp_dir("component") { tmp_dir =>
+ Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
+ check_dir(tmp_dir + Path.explode(name))
}
+ if (is_standard_component) {
+ if (ssh.is_dir(remote_contrib)) {
+ if (force) ssh.rm_tree(remote_contrib)
+ else error("Remote component directory already exists: " + remote_contrib)
+ }
+ progress.echo("Unpacking remote " + archive_name)
+ ssh.execute("tar -C " + ssh.bash_path(contrib_dir) + " -xzf " +
+ ssh.bash_path(remote_component)).check
}
-
- // remote SHA1 digests
- if (update_components_sha1) {
- val lines =
- for {
- entry <- ssh.read_dir(components_dir)
- if ssh.is_file(components_dir + Path.basic(entry)) &&
- entry.endsWith(Archive.suffix)
- }
- yield {
- progress.echo("Digesting remote " + entry)
- ssh.execute("cd " + ssh.bash_path(components_dir) +
- "; sha1sum " + Bash.string(entry)).check.out
- }
- write_components_sha1(read_components_sha1(lines))
+ else {
+ progress.echo_warning("No unpacking of non-standard component: " + archive_name)
}
}
- case s => error("Bad isabelle_components_server: " + quote(s))
+ }
+
+ // remote SHA1 digests
+ if (update_components_sha1) {
+ val lines =
+ for {
+ entry <- ssh.read_dir(components_dir)
+ if ssh.is_file(components_dir + Path.basic(entry)) &&
+ entry.endsWith(Archive.suffix)
+ }
+ yield {
+ progress.echo("Digesting remote " + entry)
+ ssh.execute("cd " + ssh.bash_path(components_dir) +
+ "; sha1sum " + Bash.string(entry)).check.out
+ }
+ write_components_sha1(read_components_sha1(lines))
+ }
}
}
--- a/src/Pure/Tools/phabricator.scala Fri Sep 16 14:02:02 2022 +0200
+++ b/src/Pure/Tools/phabricator.scala Fri Sep 16 14:26:42 2022 +0200
@@ -889,23 +889,20 @@
/* context for operations */
- def apply(user: String, host: String, port: Int = default_system_port): API =
- new API(user, host, port)
+ def apply(ssh_target: String, ssh_port: Int = default_system_port): API =
+ new API(ssh_target, ssh_port)
}
- final class API private(ssh_user: String, ssh_host: String, ssh_port: Int) {
+ final class API private(ssh_target: String, ssh_port: Int) {
/* connection */
- require(ssh_host.nonEmpty && ssh_port >= 0, "bad ssh host or port")
-
- private def ssh_user_prefix: String =
- if (ssh_user.nonEmpty) ssh_user + "@" else ""
+ require(ssh_target.nonEmpty && ssh_port >= 0, "bad ssh host or port")
private def ssh_port_suffix: String =
if (ssh_port != default_system_port) ":" + ssh_port else ""
- override def toString: String = ssh_user_prefix + ssh_host + ssh_port_suffix
- def hg_url: String = "ssh://" + ssh_user_prefix + ssh_host + ssh_port_suffix
+ override def toString: String = ssh_target + ssh_port_suffix
+ def hg_url: String = "ssh://" + ssh_target + ssh_port_suffix
/* execute methods */
@@ -915,7 +912,7 @@
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) +
+ "ssh -p " + ssh_port + " " + Bash.string(ssh_target) +
" conduit " + Bash.string(method) + " < " + File.bash_path(params_file)).check
JSON.parse(result.out, strict = false)
}