# HG changeset patch
# User wenzelm
# Date 1601666307 -7200
# Node ID 5f17bf3709b89aca87c0f590d9e8e711f7a4d8ed
# Parent  178cbf89780ee17e5a1ff64ec17b78af242a6083
clarified signature;

diff -r 178cbf89780e -r 5f17bf3709b8 src/Pure/Admin/build_sqlite.scala
--- a/src/Pure/Admin/build_sqlite.scala	Fri Oct 02 21:10:08 2020 +0200
+++ b/src/Pure/Admin/build_sqlite.scala	Fri Oct 02 21:18:27 2020 +0200
@@ -58,14 +58,7 @@
     /* jar */
 
     val jar = component_dir + Path.basic(download_name).ext("jar")
-    progress.echo("Getting " + quote(download_url))
-    try {
-      Isabelle_System.bash("curl --fail --silent --location " + Bash.string(download_url) +
-        " > " + File.bash_path(jar)).check
-    }
-    catch {
-      case ERROR(msg) => cat_error("Failed to download " + quote(download_url), msg)
-    }
+    Isabelle_System.download(download_url, jar, progress = progress)
 
     Isabelle_System.with_tmp_dir("sqlite")(jar_dir =>
     {
diff -r 178cbf89780e -r 5f17bf3709b8 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Fri Oct 02 21:10:08 2020 +0200
+++ b/src/Pure/System/isabelle_system.scala	Fri Oct 02 21:18:27 2020 +0200
@@ -368,6 +368,21 @@
     else error("Expected to find GNU tar executable")
   }
 
+  private lazy val curl_check: Unit =
+    try { bash("curl --version").check }
+    catch { case ERROR(_) => error("Cannot download files: missing curl") }
+
+  def download(url: 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) }
+  }
+
   def hostname(): String = bash("hostname -s").check.out
 
   def open(arg: String): Unit =