--- a/src/Pure/PIDE/command.ML Mon Mar 01 18:24:50 2021 +0100
+++ b/src/Pure/PIDE/command.ML Mon Mar 01 18:31:11 2021 +0100
@@ -72,7 +72,9 @@
fun read_url () =
let
- val text = Isabelle_System.download file_node;
+ val text =
+ Isabelle_System.with_tmp_file "file" "" (fn file =>
+ (Isabelle_System.download file_node file; File.read file));
val file_pos = Position.file file_node;
in (text, file_pos) end;
--- 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;