src/Pure/General/ssh.scala

       strict: Boolean = true
     ): Process_Result = {
       val args1 = Bash.string(host) + " " + Bash.string("export USER_HOME=\"$HOME\"\n" + cmd_line)
       run_command("ssh", args = args1, progress_stdout = progress_stdout,
         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))
 
 

         progress_stdout = progress_stdout,
         progress_stderr = progress_stderr,
         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()
   }
 
   object Local extends System
 }