# HG changeset patch
# User wenzelm
# Date 1614619490 -3600
# Node ID c707655239e23887d8958f8e187fa481470ed935
# Parent  4f9e4d7d38b4839066815fed0827596b122d4a2a
download more directly, via means of JVM;

diff -r 4f9e4d7d38b4 -r c707655239e2 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")