download as in Isabelle/Scala;

--- 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;