# HG changeset patch
# User wenzelm
# Date 1672328685 -3600
# Node ID 947510ce4e36fce5d5f74cc8e2dd473661f672cc
# Parent  0eb3ea050fa9906fbe8f1fbc2cfab8e96594d68e
tuned signature;

diff -r 0eb3ea050fa9 -r 947510ce4e36 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Thu Dec 29 16:17:29 2022 +0100
+++ b/src/Pure/PIDE/resources.ML	Thu Dec 29 16:44:45 2022 +0100
@@ -38,6 +38,7 @@
    {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 -> Path.T * Position.T -> Token.file
+  val read_file: Path.T -> Path.T * Position.T -> Token.file
   val parsed_files: (Path.T -> Path.T list) ->
     Token.file Exn.result list * Input.source -> theory -> Token.file list
   val parse_files: (Path.T -> Path.T list) -> (theory -> Token.file list) parser
@@ -330,7 +331,7 @@
   end;
 
 
-(* read_file_node *)
+(* read_file *)
 
 fun read_file_node file_node master_dir (src_path, pos) =
   let
@@ -358,6 +359,8 @@
   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 "";
+
 
 (* load files *)
 
@@ -374,7 +377,7 @@
           [(pos, Markup.path (Path.implode_symbolic (master_dir + src_path))),
            (pos, Markup.language_path delimited)]);
       val _ = Position.reports reports;
-    in map (read_file_node "" master_dir o rpair pos) src_paths end
+    in map (read_file master_dir o rpair pos) src_paths end
   else map Exn.release files;
 
 fun parse_files make_paths =