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