# HG changeset patch
# User wenzelm
# Date 1672239732 -3600
# Node ID 5ffe32b613ae50ad8e83e1f5ee88dab27c218ae2
# Parent  ad01b550e74b3dfc4de7902b34aae0bcb09783df
clarified modules;

diff -r ad01b550e74b -r 5ffe32b613ae src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Wed Dec 28 15:25:37 2022 +0100
+++ b/src/Pure/PIDE/command.ML	Wed Dec 28 16:02:12 2022 +0100
@@ -7,7 +7,6 @@
 signature COMMAND =
 sig
   type blob = {file_node: string, src_path: Path.T, content: (SHA1.digest * string list) option}
-  val read_file: Path.T -> Position.T -> bool -> Path.T -> Token.file
   val read_thy: Toplevel.state -> theory
   val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) ->
     blob Exn.result list * int -> Token.T list -> Toplevel.transition
@@ -57,38 +56,6 @@
 
 type blob = {file_node: string, src_path: Path.T, content: (SHA1.digest * string list) option};
 
-fun read_file_node file_node master_dir pos delimited src_path =
-  let
-    val _ =
-      if Context_Position.pide_reports ()
-      then Position.report pos (Markup.language_path delimited) else ();
-
-    fun read_local () =
-      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_remote () =
-      let
-        val text = Bytes.content (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 => read_local ()
-      | SOME (Url.File _) => read_local ()
-      | _ => read_remote ());
-
-    val lines = split_lines text;
-    val digest = SHA1.digest text;
-  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 "";
-
 local
 
 fun blob_file src_path lines digest file_node =
@@ -112,7 +79,7 @@
 
             fun make_file (Exn.Res {file_node, src_path, content = NONE}) =
                   Exn.interruptible_capture (fn () =>
-                    read_file_node file_node master_dir pos delimited src_path) ()
+                    Resources.read_file_node file_node master_dir pos delimited src_path) ()
               | make_file (Exn.Res {file_node, src_path, content = SOME (digest, lines)}) =
                   (Position.report pos (Markup.language_path delimited);
                     Exn.Res (blob_file src_path lines digest file_node))
diff -r ad01b550e74b -r 5ffe32b613ae src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Wed Dec 28 15:25:37 2022 +0100
+++ b/src/Pure/PIDE/resources.ML	Wed Dec 28 16:02:12 2022 +0100
@@ -37,6 +37,7 @@
   val check_thy: Path.T -> string ->
    {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
     imports: (string * Position.T) list, keywords: Thy_Header.keywords}
+  val read_file_node: string -> Path.T -> Position.T -> bool -> Path.T -> Token.file
   val parse_files: (Path.T -> Path.T list) -> (theory -> Token.file list) parser
   val parse_file: (theory -> Token.file) parser
   val provide: Path.T * SHA1.digest -> theory -> theory
@@ -327,6 +328,39 @@
   end;
 
 
+(* read_file_node *)
+
+fun read_file_node file_node master_dir pos delimited src_path =
+  let
+    val _ =
+      if Context_Position.pide_reports ()
+      then Position.report pos (Markup.language_path delimited) else ();
+
+    fun read_local () =
+      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_remote () =
+      let
+        val text = Bytes.content (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 => read_local ()
+      | SOME (Url.File _) => read_local ()
+      | _ => read_remote ());
+
+    val lines = split_lines text;
+    val digest = SHA1.digest text;
+  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);
+
+
 (* load files *)
 
 fun parse_files make_paths =
@@ -343,7 +377,7 @@
             src_paths |> map (fn src_path =>
               (pos, Markup.path (Path.implode_symbolic (master_dir + src_path))));
           val _ = Position.reports reports;
-        in map (Command.read_file master_dir pos delimited) src_paths end
+        in map (read_file_node "" master_dir pos delimited) src_paths end
     | files => map Exn.release files));
 
 val parse_file = parse_files single >> (fn f => f #> the_single);
diff -r ad01b550e74b -r 5ffe32b613ae src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Dec 28 15:25:37 2022 +0100
+++ b/src/Pure/ROOT.ML	Wed Dec 28 16:02:12 2022 +0100
@@ -311,9 +311,9 @@
 ML_file "Thy/document_antiquotations.ML";
 ML_file "General/graph_display.ML";
 ML_file "pure_syn.ML";
+ML_file "PIDE/resources.ML";
 ML_file "PIDE/command.ML";
 ML_file "PIDE/query_operation.ML";
-ML_file "PIDE/resources.ML";
 ML_file "Thy/thy_info.ML";
 ML_file "thm_deps.ML";
 ML_file "Thy/export_theory.ML";