--- a/src/Pure/Build/resources.ML Sat Aug 16 15:57:19 2025 +0200
+++ b/src/Pure/Build/resources.ML Sat Aug 16 16:29:20 2025 +0200
@@ -209,38 +209,38 @@
in ML_Syntax.atomic (func ^ " " ^ ML_Syntax.print_string name) end)));
-(* manage source files *)
+(* theory resources *)
-type files =
+type data =
{master_dir: Path.T, (*master directory of theory source*)
imports: (string * Position.T) list, (*source specification of imports*)
provided: (Path.T * SHA1.digest) list}; (*source path, digest*)
-fun make_files (master_dir, imports, provided): files =
+fun make_data (master_dir, imports, provided): data =
{master_dir = master_dir, imports = imports, provided = provided};
-structure Files = Theory_Data
+structure Data = Theory_Data
(
- type T = files;
- val empty = make_files (Path.current, [], []);
+ type T = data;
+ val empty = make_data (Path.current, [], []);
fun merge ({master_dir, imports, provided = provided1}, {provided = provided2, ...}) =
let val provided' = Library.merge (op =) (provided1, provided2)
- in make_files (master_dir, imports, provided') end
+ in make_data (master_dir, imports, provided') end
);
-fun map_files f =
- Files.map (fn {master_dir, imports, provided} =>
- make_files (f (master_dir, imports, provided)));
+fun map_data f =
+ Data.map (fn {master_dir, imports, provided} =>
+ make_data (f (master_dir, imports, provided)));
-val master_directory = #master_dir o Files.get;
-val imports_of = #imports o Files.get;
+val master_directory = #master_dir o Data.get;
+val imports_of = #imports o Data.get;
fun begin_theory master_dir {name, imports, keywords} parents =
let
val thy =
Theory.begin_theory name parents
- |> map_files (fn _ => (Path.explode (File.symbolic_path master_dir), imports, []))
+ |> map_data (fn _ => (Path.explode (File.symbolic_path master_dir), imports, []))
|> Thy_Header.add_keywords keywords;
val ctxt = Proof_Context.init_global thy;
val _ = List.app (ignore o check_load_command ctxt o #load_command o #2) keywords;
@@ -379,7 +379,7 @@
fun provide (src_path, digest) =
- map_files (fn (master_dir, imports, provided) =>
+ map_data (fn (master_dir, imports, provided) =>
if AList.defined (op =) provided src_path then
error ("Duplicate use of source file: " ^ Path.print src_path)
else (master_dir, imports, (src_path, digest) :: provided));
@@ -401,7 +401,7 @@
in ((full_path, digest), text) end;
fun loaded_files_current thy =
- #provided (Files.get thy) |>
+ #provided (Data.get thy) |>
forall (fn (src_path, digest) =>
(case try (load_file thy) src_path of
NONE => false