src/Pure/Tools/generated_files.ML

--- a/src/Pure/Tools/generated_files.ML	Thu Jun 23 21:25:56 2022 +0200
+++ b/src/Pure/Tools/generated_files.ML	Thu Jun 23 21:50:32 2022 +0200
@@ -6,8 +6,8 @@
 
 signature GENERATED_FILES =
 sig
-  val add_files: Path.binding * string -> theory -> theory
-  type file = {path: Path.T, pos: Position.T, content: string}
+  val add_files: Path.binding * Bytes.T -> theory -> theory
+  type file = {path: Path.T, pos: Position.T, content: Bytes.T}
   val file_binding: file -> Path.binding
   val file_markup: file -> Markup.T
   val print_file: file -> string
@@ -52,7 +52,7 @@
 
 (** context data **)
 
-type file = Path.T * (Position.T * string);
+type file = Path.T * (Position.T * Bytes.T);
 
 type file_type =
   {name: string, ext: string, make_comment: string -> string, make_string: string -> string};
@@ -75,10 +75,11 @@
   fun merge ((files1, types1, antiqs1), (files2, types2, antiqs2)) =
     let
       val files' =
-        (files1, files2) |> Symtab.join (K (Library.merge (fn ((path1, file1), (path2, file2)) =>
-          if path1 <> path2 then false
-          else if file1 = file2 then true
-          else err_dup_files path1 (#1 file1) (#1 file2))));
+        (files1, files2) |> Symtab.join (fn _ =>
+          Library.merge (fn ((path1, (pos1, bytes1)), (path2, (pos2, bytes2))) =>
+            if path1 <> path2 then false
+            else if pos1 = pos2 andalso Bytes.eq (bytes1, bytes2) then true
+            else err_dup_files path1 pos1 pos2));
       val types' = Name_Space.merge_tables (types1, types2);
       val antiqs' = Name_Space.merge_tables (antiqs1, antiqs2);
     in (files', types', antiqs') end;
@@ -104,7 +105,7 @@
 
 (* get files *)
 
-type file = {path: Path.T, pos: Position.T, content: string};
+type file = {path: Path.T, pos: Position.T, content: Bytes.T};
 
 fun file_binding (file: file) = Path.binding (#path file, #pos file);
 
@@ -147,11 +148,15 @@
   let
     val path = Path.expand (dir + #path file);
     val _ = Isabelle_System.make_directory (Path.dir path);
-    val _ = File.generate path (#content file);
-  in () end;
+    val content = #content file;
+    val write_content =
+      (case try Bytes.read path of
+        SOME old_content => not (Bytes.eq (content, old_content))
+      | NONE => true)
+  in if write_content then Bytes.write path content else () end;
 
 fun export_file thy (file: file) =
-  Export.export thy (file_binding file) [XML.Text (#content file)];
+  Export.export thy (file_binding file) (Bytes.contents_blob (#content file));
 
 
 (* file types *)
@@ -244,7 +249,7 @@
         handle ERROR msg => error (msg ^ Position.here pos);
 
     val header = #make_comment file_type " generated by Isabelle ";
-    val content = header ^ "\n" ^ read_source lthy file_type source;
+    val content = Bytes.string (header ^ "\n" ^ read_source lthy file_type source);
   in lthy |> (Local_Theory.background_theory o add_files) (binding, content) end;
 
 fun generate_file_cmd (file, source) lthy =
@@ -297,15 +302,15 @@
               val binding = binding0 |> Path.map_binding (executable = SOME true ? Path.exe);
               val (path, pos) = Path.dest_binding binding;
               val content =
-                (case try File.read (dir + path) of
-                  SOME context => context
+                (case try Bytes.read (dir + path) of
+                  SOME bytes => Bytes.contents_blob bytes
                 | NONE => error ("Missing result file " ^ Path.print path ^ Position.here pos));
               val _ = Export.report_export thy export_prefix;
               val binding' =
                 Path.map_binding (Path.append (Path.path_of_binding export_prefix)) binding;
             in
               (if is_some executable then Export.export_executable else Export.export)
-                thy binding' [XML.Text content]
+                thy binding' content
             end));
       val _ =
         if null export then ()