# HG changeset patch
# User wenzelm
# Date 1754994631 -7200
# Node ID 9dc2e315525785de6f85d945380e34b39b23f424
# Parent  3300a2aadc3aa08d6035352d031f7dd7345c9b0d
tuned signature;

diff -r 3300a2aadc3a -r 9dc2e3155257 src/Pure/Build/resources.ML
--- a/src/Pure/Build/resources.ML	Tue Aug 12 11:56:18 2025 +0200
+++ b/src/Pure/Build/resources.ML	Tue Aug 12 12:30:31 2025 +0200
@@ -378,11 +378,11 @@
 val parse_file = parse_files single >> (fn f => f #> the_single);
 
 
-fun provide (src_path, id) =
+fun provide (src_path, digest) =
   map_files (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, id) :: provided));
+    else (master_dir, imports, (src_path, digest) :: provided));
 
 fun provide_file (file: Token.file) = provide (#src_path file, #digest file);
 fun provide_file' file thy = (file, provide_file file thy);
@@ -397,15 +397,15 @@
   let
     val full_path = check_file (master_directory thy) src_path;
     val text = File.read full_path;
-    val id = SHA1.digest text;
-  in ((full_path, id), text) end;
+    val digest = SHA1.digest text;
+  in ((full_path, digest), text) end;
 
 fun loaded_files_current thy =
   #provided (Files.get thy) |>
-    forall (fn (src_path, id) =>
+    forall (fn (src_path, digest) =>
       (case try (load_file thy) src_path of
         NONE => false
-      | SOME ((_, id'), _) => id = id'));
+      | SOME ((_, digest'), _) => digest = digest'));
 
 
 (* formal check *)