diff -r c707655239e2 -r ff7ce802be52 src/Pure/System/isabelle_system.ML --- a/src/Pure/System/isabelle_system.ML Mon Mar 01 18:24:50 2021 +0100 +++ b/src/Pure/System/isabelle_system.ML Mon Mar 01 18:31:11 2021 +0100 @@ -19,7 +19,7 @@ val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a val rm_tree: Path.T -> unit val with_tmp_dir: string -> (Path.T -> 'a) -> 'a - val download: string -> string + val download: string -> Path.T -> unit end; structure Isabelle_System: ISABELLE_SYSTEM = @@ -111,9 +111,7 @@ (* download file *) -fun download url = - with_tmp_file "download" "" (fn path => - (Scala.function_thread "download" (cat_strings0 [url, absolute_path path]); - File.read path)); +fun download url file = + ignore (Scala.function_thread "download" (cat_strings0 [url, absolute_path file])); end;