# HG changeset patch
# User wenzelm
# Date 1672245574 -3600
# Node ID 25900fbea7ad158282bfd532f146b0a10951f182
# Parent  797621be9317e9bca9040686ab0065ceb69426df
tuned signature, for the sake of AFP/Isabelle_C;

diff -r 797621be9317 -r 25900fbea7ad src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Wed Dec 28 16:49:43 2022 +0100
+++ b/src/Pure/PIDE/resources.ML	Wed Dec 28 17:39:34 2022 +0100
@@ -38,6 +38,8 @@
    {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 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
   val parse_file: (theory -> Token.file) parser
   val provide: Path.T * SHA1.digest -> theory -> theory
@@ -359,23 +361,24 @@
 
 (* load files *)
 
+fun parsed_files make_paths (files, source) thy =
+  if null files then
+    let
+      val master_dir = master_directory thy;
+      val name = Input.string_of source;
+      val pos = Input.pos_of source;
+      val delimited = Input.is_delimited source;
+      val src_paths = make_paths (Path.explode name);
+      val reports =
+        src_paths |> maps (fn src_path =>
+          [(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
+  else map Exn.release files;
+
 fun parse_files make_paths =
-  Scan.ahead Parse.not_eof -- Parse.path_input >> (fn (tok, source) => fn thy =>
-    (case Token.get_files tok of
-      [] =>
-        let
-          val master_dir = master_directory thy;
-          val name = Input.string_of source;
-          val pos = Input.pos_of source;
-          val delimited = Input.is_delimited source;
-          val src_paths = make_paths (Path.explode name);
-          val reports =
-            src_paths |> maps (fn src_path =>
-              [(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
-    | files => map Exn.release files));
+  (Scan.ahead Parse.not_eof >> Token.get_files) -- Parse.path_input >> parsed_files make_paths;
 
 val parse_file = parse_files single >> (fn f => f #> the_single);