# HG changeset patch
# User wenzelm
# Date 1614458218 -3600
# Node ID c2ab1a970e82500bf8f874649df12b8aad5c1ce8
# Parent  5b15eee1a661bd8f967f77ee9f7d89487cddf6bc
more Isabelle/ML/Scala operations;

diff -r 5b15eee1a661 -r c2ab1a970e82 NEWS
--- a/NEWS	Sat Feb 27 21:01:07 2021 +0100
+++ b/NEWS	Sat Feb 27 21:36:58 2021 +0100
@@ -73,6 +73,7 @@
   - Isabelle_System.copy_dir
   - Isabelle_System.copy_file
   - Isabelle_System.copy_base_file
+  - Isabelle_System.download
 
 
 
diff -r 5b15eee1a661 -r c2ab1a970e82 src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Sat Feb 27 21:01:07 2021 +0100
+++ b/src/Pure/System/isabelle_system.ML	Sat Feb 27 21:36:58 2021 +0100
@@ -114,12 +114,7 @@
 
 fun download url =
   with_tmp_file "download" "" (fn path =>
-    let
-      val s = "curl --fail --silent --location " ^ Bash.string url ^ " > " ^ File.bash_path path;
-      val res = bash_process s;
-    in
-      if Process_Result.ok res then File.read path
-      else cat_error ("Failed to download " ^ quote url) (Process_Result.err res)
-    end);
+   (Scala.function "download" (url ^ "\000" ^ Path.implode (File.absolute_path path));
+    File.read path));
 
 end;
diff -r 5b15eee1a661 -r c2ab1a970e82 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Feb 27 21:01:07 2021 +0100
+++ b/src/Pure/System/isabelle_system.scala	Sat Feb 27 21:36:58 2021 +0100
@@ -489,21 +489,6 @@
     }
   }
 
-  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 =
-  {
-    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 =
@@ -552,4 +537,31 @@
       case None => getenv_strict("ISABELLE_LOGIC")
     }
   }
+
+
+  /* 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 =
+  {
+    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) }
+  }
+
+  object Download extends Scala.Fun("download")
+  {
+    val here = Scala_Project.here
+    def apply(arg: String): String =
+      Library.space_explode('\u0000', arg) match {
+        case List(url, file) => download(url, Path.explode(file)); ""
+      }
+  }
 }
diff -r 5b15eee1a661 -r c2ab1a970e82 src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Sat Feb 27 21:01:07 2021 +0100
+++ b/src/Pure/System/scala.scala	Sat Feb 27 21:36:58 2021 +0100
@@ -249,4 +249,5 @@
   Isabelle_System.Copy_Dir,
   Isabelle_System.Copy_File,
   Isabelle_System.Copy_File_Base,
+  Isabelle_System.Download,
   Isabelle_Tool.Isabelle_Tools)