support remote download_file;
authorwenzelm
Mon, 23 Jan 2023 15:43:09 +0100
changeset 77054 3bb374ac31b3
parent 77053 c839b84ee66f
child 77055 f56800b8b085
support remote download_file;
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()
   }