# HG changeset patch
# User wenzelm
# Date 1608332458 -3600
# Node ID f3d0e4ea492d5b2180130ee714f1b932d0cf8e78
# Parent  19484bb038a8d442908558bbdeb660c95c9c9d5a
download as in Isabelle/Scala;

diff -r 19484bb038a8 -r f3d0e4ea492d src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Fri Dec 18 23:30:29 2020 +0100
+++ b/src/Pure/System/isabelle_system.ML	Sat Dec 19 00:00:58 2020 +0100
@@ -20,6 +20,7 @@
   val create_tmp_path: string -> string -> Path.T
   val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a
   val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
+  val download: string -> string
 end;
 
 structure Isabelle_System: ISABELLE_SYSTEM =
@@ -120,4 +121,14 @@
   let val path = create_tmp_path name ""
   in Exn.release (Exn.capture f (make_directory path) before ignore (try rm_tree path)) end;
 
+
+(* download file *)
+
+fun download url =
+  with_tmp_file "download" "" (fn path =>
+    ("curl --fail --silent --location " ^ Bash.string url ^ " > " ^ File.bash_path path)
+    |> Bash.process
+    |> (fn {rc = 0, ...} => File.read path
+         | {err, ...} => cat_error ("Failed to download " ^ quote url) err));
+
 end;