# HG changeset patch
# User wenzelm
# Date 1614619871 -3600
# Node ID ff7ce802be52824d4da87c5492741586cd5b478a
# Parent  c707655239e23887d8958f8e187fa481470ed935
clarified signature, according to Isabelle/Scala;

diff -r c707655239e2 -r ff7ce802be52 src/Pure/PIDE/command.ML
--- 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;
 
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;