--- 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 =>
{
--- 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 =