# HG changeset patch
# User wenzelm
# Date 1608332894 -3600
# Node ID ac6457a70db5d52ca873d1cac635843fe166d724
# Parent  854ebb9e4eb358b66d22c89606a9de0fa628b9cc
download auxiliary files via "curl";

diff -r 854ebb9e4eb3 -r ac6457a70db5 NEWS
--- a/NEWS	Sat Dec 19 00:04:32 2020 +0100
+++ b/NEWS	Sat Dec 19 00:08:14 2020 +0100
@@ -19,6 +19,9 @@
 * Improved markup for theory header imports: hyperlinks for theory files
 work without formal checking of content.
 
+* The prover process can download auxiliary files (e.g. 'ML_file') for
+theories with remote URL. This requires the external "curl" program.
+
 * Action "isabelle.goto-entity" (shortcut CS+d) jumps to the definition
 of the formal entity at the caret position.
 
diff -r 854ebb9e4eb3 -r ac6457a70db5 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sat Dec 19 00:04:32 2020 +0100
+++ b/src/Pure/PIDE/command.ML	Sat Dec 19 00:08:14 2020 +0100
@@ -60,19 +60,29 @@
     val _ =
       if Context_Position.pide_reports ()
       then Position.report pos (Markup.language_path delimited) else ();
-    val _ =
+
+    fun read_file () =
+      let
+        val path = File.check_file (File.full_path master_dir src_path);
+        val text = File.read path;
+        val file_pos = Path.position path;
+      in (text, file_pos) end;
+
+    fun read_url () =
+      let
+        val text = Isabelle_System.download file_node;
+        val file_pos = Position.file file_node;
+      in (text, file_pos) end;
+
+    val (text, file_pos) =
       (case try Url.explode file_node of
-        NONE => ()
-      | SOME (Url.File _) => ()
-      | _ =>
-          error ("Prover cannot load remote file " ^
-            Markup.markup (Markup.url file_node) (quote file_node)));
-    val full_path = File.check_file (File.full_path master_dir src_path);
-    val text = File.read full_path;
+        NONE => read_file ()
+      | SOME (Url.File _) => read_file ()
+      | _ => read_url ());
+
     val lines = split_lines text;
     val digest = SHA1.digest text;
-    val file_pos = Position.copy_id pos (Path.position full_path);
-  in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end
+  in {src_path = src_path, lines = lines, digest = digest, pos = Position.copy_id pos file_pos} end
   handle ERROR msg => error (msg ^ Position.here pos);
 
 val read_file = read_file_node "";