--- 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)
--- 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
--- 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
--- 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(
--- 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 =>
{
--- 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)
--- 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)
--- 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;
--- 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 *)
--- 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) }
}
}
--- 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)