# HG changeset patch
# User wenzelm
# Date 1618244974 -7200
# Node ID 4e6b31ed71970a6fe86a9e96857dbd41f2b69e30
# Parent  1aa92bc4d356a192d3e9f610e75ae69baf08a04f
clarified signature: avoid tmp file;

diff -r 1aa92bc4d356 -r 4e6b31ed7197 src/Pure/Admin/build_csdp.scala
--- a/src/Pure/Admin/build_csdp.scala	Mon Apr 12 18:10:13 2021 +0200
+++ b/src/Pure/Admin/build_csdp.scala	Mon Apr 12 18:29:34 2021 +0200
@@ -97,7 +97,7 @@
       /* download source */
 
       val archive_path = tmp_dir + Path.basic(archive_name)
-      Isabelle_System.download(download_url, archive_path, progress = progress)
+      Isabelle_System.download_file(download_url, archive_path, progress = progress)
 
       Isabelle_System.bash("tar xzf " + File.bash_path(archive_path), cwd = tmp_dir.file).check
       val source_name = File.get_dir(tmp_dir)
diff -r 1aa92bc4d356 -r 4e6b31ed7197 src/Pure/Admin/build_e.scala
--- a/src/Pure/Admin/build_e.scala	Mon Apr 12 18:10:13 2021 +0200
+++ b/src/Pure/Admin/build_e.scala	Mon Apr 12 18:29:34 2021 +0200
@@ -40,7 +40,7 @@
 
       val archive_url = download_url + "/V_" + version + "/E.tgz"
       val archive_path = tmp_dir + Path.explode("E.tgz")
-      Isabelle_System.download(archive_url, archive_path, progress = progress)
+      Isabelle_System.download_file(archive_url, archive_path, progress = progress)
 
       Isabelle_System.bash("tar xzf " + archive_path, cwd = tmp_dir.file).check
       Isabelle_System.bash("tar xzf " + archive_path + " && mv E src", cwd = component_dir.file).check
diff -r 1aa92bc4d356 -r 4e6b31ed7197 src/Pure/Admin/build_jcef.scala
--- a/src/Pure/Admin/build_jcef.scala	Mon Apr 12 18:10:13 2021 +0200
+++ b/src/Pure/Admin/build_jcef.scala	Mon Apr 12 18:29:34 2021 +0200
@@ -57,7 +57,7 @@
       Isabelle_System.with_tmp_file("archive", ext = "zip")(archive_file =>
       {
         val url = base_url + "/" + Url.encode(version) + "/" + platform.archive
-        Isabelle_System.download(url, archive_file, progress = progress)
+        Isabelle_System.download_file(url, archive_file, progress = progress)
         Isabelle_System.bash("unzip -x " + File.bash_path(archive_file),
             cwd = component_dir.file).check
 
diff -r 1aa92bc4d356 -r 4e6b31ed7197 src/Pure/Admin/build_spass.scala
--- a/src/Pure/Admin/build_spass.scala	Mon Apr 12 18:10:13 2021 +0200
+++ b/src/Pure/Admin/build_spass.scala	Mon Apr 12 18:29:34 2021 +0200
@@ -66,7 +66,7 @@
       /* download source */
 
       val archive_path = tmp_dir + Path.basic(archive_name)
-      Isabelle_System.download(download_url, archive_path, progress = progress)
+      Isabelle_System.download_file(download_url, archive_path, progress = progress)
 
       Isabelle_System.bash("tar xzf " + archive_path, cwd = tmp_dir.file).check
       Isabelle_System.bash(
diff -r 1aa92bc4d356 -r 4e6b31ed7197 src/Pure/Admin/build_sqlite.scala
--- a/src/Pure/Admin/build_sqlite.scala	Mon Apr 12 18:10:13 2021 +0200
+++ b/src/Pure/Admin/build_sqlite.scala	Mon Apr 12 18:29:34 2021 +0200
@@ -53,7 +53,7 @@
     /* jar */
 
     val jar = component_dir + Path.basic(download_name).ext("jar")
-    Isabelle_System.download(download_url, jar, progress = progress)
+    Isabelle_System.download_file(download_url, jar, progress = progress)
 
     Isabelle_System.with_tmp_dir("sqlite")(jar_dir =>
     {
diff -r 1aa92bc4d356 -r 4e6b31ed7197 src/Pure/Admin/build_verit.scala
--- a/src/Pure/Admin/build_verit.scala	Mon Apr 12 18:10:13 2021 +0200
+++ b/src/Pure/Admin/build_verit.scala	Mon Apr 12 18:29:34 2021 +0200
@@ -60,7 +60,7 @@
       /* download source */
 
       val archive_path = tmp_dir + Path.basic(archive_name)
-      Isabelle_System.download(download_url, archive_path, progress = progress)
+      Isabelle_System.download_file(download_url, archive_path, progress = progress)
 
       Isabelle_System.bash("tar xzf " + File.bash_path(archive_path), cwd = tmp_dir.file).check
       val source_name = File.get_dir(tmp_dir)
diff -r 1aa92bc4d356 -r 4e6b31ed7197 src/Pure/Admin/components.scala
--- a/src/Pure/Admin/components.scala	Mon Apr 12 18:10:13 2021 +0200
+++ b/src/Pure/Admin/components.scala	Mon Apr 12 18:29:34 2021 +0200
@@ -67,7 +67,7 @@
       val archive = base_dir + Path.explode(archive_name)
       if (!archive.is_file) {
         val remote = Components.default_component_repository + "/" + archive_name
-        Isabelle_System.download(remote, archive, progress = progress)
+        Isabelle_System.download_file(remote, archive, progress = progress)
       }
       for (dir <- copy_dir) {
         Isabelle_System.make_directory(dir)
diff -r 1aa92bc4d356 -r 4e6b31ed7197 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Mon Apr 12 18:10:13 2021 +0200
+++ b/src/Pure/PIDE/command.ML	Mon Apr 12 18:29:34 2021 +0200
@@ -72,9 +72,7 @@
 
     fun read_url () =
       let
-        val text =
-          Isabelle_System.with_tmp_file "file" "" (fn file =>
-            (Isabelle_System.download file_node file; File.read file));
+        val text = Isabelle_System.download file_node;
         val file_pos = Position.file file_node;
       in (text, file_pos) end;
 
diff -r 1aa92bc4d356 -r 4e6b31ed7197 src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Mon Apr 12 18:10:13 2021 +0200
+++ b/src/Pure/System/isabelle_system.ML	Mon Apr 12 18:29:34 2021 +0200
@@ -20,7 +20,8 @@
   val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a
   val rm_tree: Path.T -> unit
   val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
-  val download: string -> Path.T -> unit
+  val download: string -> string
+  val download_file: string -> Path.T -> unit
   val isabelle_id: unit -> string
   val isabelle_identifier: unit -> string option
   val isabelle_heading: unit -> string
@@ -116,8 +117,9 @@
 
 (* download file *)
 
-fun download url file =
-  ignore (Scala.function "download" [url, absolute_path file]);
+val download = Scala.function1 "download";
+
+fun download_file url path = File.write path (download url);
 
 
 (* Isabelle distribution identification *)
diff -r 1aa92bc4d356 -r 4e6b31ed7197 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Apr 12 18:10:13 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala	Mon Apr 12 18:29:34 2021 +0200
@@ -594,22 +594,21 @@
 
   /* download file */
 
-  def download(url_name: String, file: Path, progress: Progress = new Progress): Unit =
+  def download(url_name: String, progress: Progress = new Progress): HTTP.Content =
   {
     val url = Url(url_name)
     progress.echo("Getting " + quote(url_name))
-    val content =
-      try { HTTP.Client.get(url) }
-      catch { case ERROR(msg) => cat_error("Failed to download " + quote(url_name), msg) }
-    Bytes.write(file, content.bytes)
+    try { HTTP.Client.get(url) }
+    catch { case ERROR(msg) => cat_error("Failed to download " + quote(url_name), msg) }
   }
 
-  object Download extends Scala.Fun_Strings("download", thread = true)
+  def download_file(url_name: String, file: Path, progress: Progress = new Progress): Unit =
+    Bytes.write(file, download(url_name, progress = progress).bytes)
+
+  object Download extends Scala.Fun("download", thread = true)
   {
     val here = Scala_Project.here
-    override def apply(args: List[String]): List[String] =
-      args match {
-        case List(url, file) => download(url, Path.explode(file)); Nil
-      }
+    override def invoke(args: List[Bytes]): List[Bytes] =
+      args match { case List(url) => List(download(url.text).bytes) }
   }
 }
diff -r 1aa92bc4d356 -r 4e6b31ed7197 src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Mon Apr 12 18:10:13 2021 +0200
+++ b/src/Pure/Tools/phabricator.scala	Mon Apr 12 18:29:34 2021 +0200
@@ -209,7 +209,7 @@
       val archive =
         if (Url.is_wellformed(mercurial_source)) {
           val archive = tmp_dir + Path.basic("mercurial.tar.gz")
-          Isabelle_System.download(mercurial_source, archive)
+          Isabelle_System.download_file(mercurial_source, archive)
           archive
         }
         else Path.explode(mercurial_source)