--- 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);