# HG changeset patch
# User wenzelm
# Date 1674484989 -3600
# Node ID 3bb374ac31b335d047573617a23441141ff27396
# Parent  c839b84ee66f73fdf71c220a6bdcd35e465f84a1
support remote download_file;

diff -r c839b84ee66f -r 3bb374ac31b3 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Mon Jan 23 15:15:19 2023 +0100
+++ b/src/Pure/General/ssh.scala	Mon Jan 23 15:43:09 2023 +0100
@@ -190,6 +190,19 @@
         progress_stderr = progress_stderr, strict = strict)
     }
 
+    override def download_file(
+      url_name: String,
+      file: Path,
+      progress: Progress = new Progress
+    ): Unit = {
+      val cmd_line =
+        File.read(Path.explode("~~/lib/scripts/download_file")) + "\n" +
+          "download_file " + Bash.string(url_name) + " " + bash_path(file)
+      execute(cmd_line,
+        progress_stdout = progress.echo,
+        progress_stderr = progress.echo).check
+    }
+
     override lazy val isabelle_platform: Isabelle_Platform = Isabelle_Platform(ssh = Some(ssh))
 
 
@@ -355,6 +368,9 @@
         env = if (settings) Isabelle_System.settings() else null,
         strict = strict)
 
+    def download_file(url_name: String, file: Path, progress: Progress = new Progress): Unit =
+      Isabelle_System.download_file(url_name, file, progress = progress)
+
     def isabelle_platform: Isabelle_Platform = Isabelle_Platform()
   }