download more directly, via means of JVM;
authorwenzelm
Mon, 01 Mar 2021 18:24:50 +0100
changeset 73585 c707655239e2
parent 73584 4f9e4d7d38b4
child 73586 ff7ce802be52
download more directly, via means of JVM;
src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Mar 01 18:24:27 2021 +0100
+++ b/src/Pure/System/isabelle_system.scala	Mon Mar 01 18:24:50 2021 +0100
@@ -14,8 +14,6 @@
 import java.nio.file.attribute.BasicFileAttributes
 
 
-import scala.annotation.tailrec
-
 
 object Isabelle_System
 {
@@ -549,19 +547,14 @@
 
   /* download file */
 
-  private lazy val curl_check: Unit =
-    try { require_command("curl") }
-    catch { case ERROR(msg) => error(msg + " --- cannot download files") }
-
-  def download(url: String, file: Path, progress: Progress = new Progress): Unit =
+  def download(url_name: String, file: Path, progress: Progress = new Progress): Unit =
   {
-    curl_check
-    progress.echo("Getting " + quote(url))
-    try {
-      bash("curl --fail --silent --location " + Bash.string(url) +
-        " > " + File.bash_path(file)).check
-    }
-    catch { case ERROR(msg) => cat_error("Failed to download " + quote(url), msg) }
+    val url = Url(url_name)
+    progress.echo("Getting " + quote(url_name))
+    val bytes =
+      try { Url.read_bytes(url) }
+      catch { case ERROR(msg) => cat_error("Failed to download " + quote(url_name), msg) }
+    Bytes.write(file, bytes)
   }
 
   object Download extends Scala.Fun("download")