src/Pure/System/components.scala
changeset 77059 422c57b75b17
parent 77058 44f79689115d
child 77066 72d87e32b062
--- 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)
     }
   }