support remote operations;

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

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