--- 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)
}
}