# HG changeset patch # User wenzelm # Date 1674509117 -3600 # Node ID 422c57b75b170f0b9f393bb93b8e099342a6f471 # Parent 44f79689115dc77525a91d73b4cf5c8b69f08770 support remote operations; diff -r 44f79689115d -r 422c57b75b17 src/Pure/General/ssh.scala --- a/src/Pure/General/ssh.scala Mon Jan 23 20:27:46 2023 +0100 +++ b/src/Pure/General/ssh.scala Mon Jan 23 22:25:17 2023 +0100 @@ -226,6 +226,14 @@ path } + override def copy_file(src: Path, dst: Path): Unit = { + val direct = if (is_dir(dst)) "/." else "" + if (!execute("cp -a " + bash_path(src) + " " + bash_path(dst) + direct).ok) { + error("Failed to copy file " + expand_path(src) + " to " + + expand_path(dst) + " (ssh " + toString + ")") + } + } + def read_dir(path: Path): List[String] = run_sftp("@cd " + sftp_path(path) + "\n@ls -1 -a").out_lines.flatMap(s => if (s == "." || s == "..") None @@ -352,6 +360,7 @@ def is_file(path: Path): Boolean = path.is_file def make_directory(path: Path): Path = Isabelle_System.make_directory(path) def with_tmp_dir[A](body: Path => A): A = Isabelle_System.with_tmp_dir("tmp")(body) + def copy_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2) def read_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2) def write_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path2, path1) def read_bytes(path: Path): Bytes = Bytes.read(path) diff -r 44f79689115d -r 422c57b75b17 src/Pure/System/components.scala --- a/src/Pure/System/components.scala Mon Jan 23 20:27:46 2023 +0100 +++ b/src/Pure/System/components.scala Mon Jan 23 22:25:17 2023 +0100 @@ -48,33 +48,43 @@ def contrib(dir: Path = Path.current, name: String = ""): Path = dir + Path.explode("contrib") + Path.explode(name) - def unpack(dir: Path, archive: Path, progress: Progress = new Progress): String = { + def unpack( + dir: Path, + archive: Path, + ssh: SSH.System = SSH.Local, + progress: Progress = new Progress + ): String = { val name = Archive.get_name(archive.file_name) progress.echo("Unpacking " + name) - Isabelle_System.bash( - "tar -C " + File.bash_path(dir) + " -x -z -f " + File.bash_path(archive)).check + ssh.execute( + "tar -C " + File.bash_path(dir) + " -x -z -f " + File.bash_path(archive), + progress_stdout = progress.echo, + progress_stderr = progress.echo).check name } - def resolve(base_dir: Path, names: List[String], + def resolve( + base_dir: Path, + names: List[String], target_dir: Option[Path] = None, copy_dir: Option[Path] = None, component_repository: String = Components.default_component_repository, + ssh: SSH.System = SSH.Local, progress: Progress = new Progress ): Unit = { - Isabelle_System.make_directory(base_dir) + ssh.make_directory(base_dir) for (name <- names) { val archive_name = Archive(name) val archive = base_dir + Path.explode(archive_name) - if (!archive.is_file) { + if (!ssh.is_file(archive)) { val remote = Url.append_path(component_repository, archive_name) - Isabelle_System.download_file(remote, archive, progress = progress) + ssh.download_file(remote, archive, progress = progress) } for (dir <- copy_dir) { - Isabelle_System.make_directory(dir) - Isabelle_System.copy_file(archive, dir) + ssh.make_directory(dir) + ssh.copy_file(archive, dir) } - unpack(target_dir getOrElse base_dir, archive, progress = progress) + unpack(target_dir getOrElse base_dir, archive, ssh = ssh, progress = progress) } }