more scalable generated files and code export, using Bytes.T;

--- a/src/HOL/Library/code_test.ML	Thu Jun 23 21:25:56 2022 +0200
+++ b/src/HOL/Library/code_test.ML	Thu Jun 23 21:50:32 2022 +0200
@@ -153,7 +153,8 @@
       | SOME drv => drv)
     val with_dir = if Config.get ctxt debug then with_debug_dir else Isabelle_System.with_tmp_dir
     fun eval result =
-      with_dir "Code_Test" (driver ctxt ((apfst o map o apfst) Long_Name.implode result))
+      with_dir "Code_Test"
+        (driver ctxt ((apfst o map) (apfst Long_Name.implode #> apsnd Bytes.content) result))
       |> parse_result compiler
     fun evaluator program _ vs_ty deps =
       Exn.interruptible_capture eval

--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Jun 23 21:25:56 2022 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Jun 23 21:50:32 2022 +0200
@@ -215,8 +215,9 @@
   |> Exn.release
 
 fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size))
-    ctxt cookie (code_modules, _) =
+    ctxt cookie (code_modules_bytes, _) =
   let
+    val code_modules = (map o apsnd) Bytes.content code_modules_bytes
     val ((is_genuine, counterexample_of), (get, put, put_ml)) = cookie
     fun message s = if quiet then () else writeln s
     fun verbose_message s = if not quiet andalso verbose then writeln s else ()

--- a/src/Pure/General/file.ML	Thu Jun 23 21:25:56 2022 +0200
+++ b/src/Pure/General/file.ML	Thu Jun 23 21:50:32 2022 +0200
@@ -34,7 +34,6 @@
   val read: Path.T -> string
   val write: Path.T -> string -> unit
   val append: Path.T -> string -> unit
-  val generate: Path.T -> string -> unit
   val output: BinIO.outstream -> string -> unit
   val outputs: BinIO.outstream -> string list -> unit
   val write_list: Path.T -> string list -> unit
@@ -170,7 +169,6 @@
 
 fun write path txt = write_list path [txt];
 fun append path txt = append_list path [txt];
-fun generate path txt = if try read path = SOME txt then () else write path txt;
 
 fun write_buffer path buf =
   open_output (fn file => List.app (output file) (Buffer.contents buf)) path;

--- a/src/Pure/Thy/export.ML	Thu Jun 23 21:25:56 2022 +0200
+++ b/src/Pure/Thy/export.ML	Thu Jun 23 21:50:32 2022 +0200
@@ -53,10 +53,10 @@
     {theory = thy, binding = binding, executable = true, compress = true, strict = true} body;
 
 fun export_file thy binding file =
-  export thy binding [XML.Text (File.read file)];
+  export thy binding (Bytes.contents_blob (Bytes.read file));
 
 fun export_executable_file thy binding file =
-  export_executable thy binding [XML.Text (File.read file)];
+  export_executable thy binding (Bytes.contents_blob (Bytes.read file));
 
 
 (* information message *)

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

--- a/src/Tools/Code/code_printer.ML	Thu Jun 23 21:25:56 2022 +0200
+++ b/src/Tools/Code/code_printer.ML	Thu Jun 23 21:50:32 2022 +0200
@@ -26,7 +26,7 @@
   val doublesemicolon: Pretty.T list -> Pretty.T
   val indent: int -> Pretty.T -> Pretty.T
   val markup_stmt: Code_Symbol.T -> Pretty.T -> Pretty.T
-  val format: Code_Symbol.T list -> int -> Pretty.T -> string
+  val format: Code_Symbol.T list -> int -> Pretty.T -> Bytes.T
 
   type var_ctxt
   val make_vars: string list -> var_ctxt
@@ -165,7 +165,7 @@
   #> YXML.parse_body
   #> filter_presentation presentation_names
   #> Buffer.add "\n"
-  #> Buffer.content;
+  #> Bytes.buffer;
 
 
 (** names and variable name contexts **)

--- a/src/Tools/Code/code_runtime.ML	Thu Jun 23 21:25:56 2022 +0200
+++ b/src/Tools/Code/code_runtime.ML	Thu Jun 23 21:50:32 2022 +0200
@@ -92,7 +92,7 @@
 
 fun build_compilation_text ctxt some_target program consts =
   Code_Target.compilation_text ctxt (the_default target some_target) program consts false
-  #>> (fn ml_modules => space_implode "\n\n" (map snd ml_modules));
+  #>> (fn ml_modules => space_implode "\n\n" (map (Bytes.content o snd) ml_modules));
 
 fun run_compilation_text cookie ctxt comp vs_t args =
   let
@@ -439,7 +439,7 @@
     val (ml_modules, target_names) =
       Code_Target.produce_code_for ctxt
         target module_name NONE [] program false (map Constant consts @ map Type_Constructor tycos);
-    val ml_code = space_implode "\n\n" (map snd ml_modules);
+    val ml_code = space_implode "\n\n" (map (Bytes.content o snd) ml_modules);
     val (consts', tycos') = chop (length consts) target_names;
     val consts_map = map2 (fn const =>
       fn NONE =>
@@ -482,7 +482,7 @@
         | SOME c' => c';
     val tyco_names =  map deresolve_tyco named_tycos;
     val const_names = map deresolve_const named_consts;
-    val generated_code = space_implode "\n\n" (map snd ml_modules);
+    val generated_code = space_implode "\n\n" (map (Bytes.content o snd) ml_modules);
     val (of_term_code, of_term_names) =
       print_computation_code ctxt compiled_value computation_cTs computation_Ts;
     val compiled_computation = generated_code ^ "\n" ^ of_term_code;
@@ -720,7 +720,7 @@
           "(* Generated from " ^
             Path.implode (Resources.thy_path (Path.basic (Context.theory_name thy))) ^
           "; DO NOT EDIT! *)";
-        val thy' = Code_Target.export code_binding (preamble ^ "\n\n" ^ code) thy;
+        val thy' = Code_Target.export code_binding (Bytes.string (preamble ^ "\n\n" ^ code)) thy;
         val _ = Code_Target.code_export_message thy';
       in thy' end;
 

--- a/src/Tools/Code/code_target.ML	Thu Jun 23 21:25:56 2022 +0200
+++ b/src/Tools/Code/code_target.ML	Thu Jun 23 21:50:32 2022 +0200
@@ -16,9 +16,9 @@
     -> int option -> Token.T list  -> Code_Thingol.program -> bool -> Code_Symbol.T list
     -> local_theory -> local_theory
   val produce_code_for: Proof.context -> string -> string -> int option -> Token.T list
-    -> Code_Thingol.program -> bool -> Code_Symbol.T list -> (string list * string) list * string option list
+    -> Code_Thingol.program -> bool -> Code_Symbol.T list -> (string list * Bytes.T) list * string option list
   val present_code_for: Proof.context -> string -> string -> int option -> Token.T list
-    -> Code_Thingol.program -> Code_Symbol.T list * Code_Symbol.T list -> string
+    -> Code_Thingol.program -> Code_Symbol.T list * Code_Symbol.T list -> Bytes.T
   val check_code_for: string -> bool -> Token.T list
     -> Code_Thingol.program -> bool -> Code_Symbol.T list -> local_theory -> local_theory
 
@@ -29,9 +29,9 @@
     -> (((string * string) * ({physical: bool} * Input.source) option) * Token.T list) list
     -> local_theory -> local_theory
   val produce_code: Proof.context -> bool -> string list
-    -> string -> string -> int option -> Token.T list -> (string list * string) list * string option list
+    -> string -> string -> int option -> Token.T list -> (string list * Bytes.T) list * string option list
   val present_code: Proof.context -> string list -> Code_Symbol.T list
-    -> string -> string -> int option -> Token.T list -> string
+    -> string -> string -> int option -> Token.T list -> Bytes.T
   val check_code: bool -> string list -> ((string * bool) * Token.T list) list
     -> local_theory -> local_theory
 
@@ -39,13 +39,13 @@
   val generatedN: string
   val code_path: Path.T -> Path.T
   val code_export_message: theory -> unit
-  val export: Path.binding -> string -> theory -> theory
+  val export: Path.binding -> Bytes.T -> theory -> theory
   val compilation_text: Proof.context -> string -> Code_Thingol.program
     -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
-    -> (string list * string) list * string
+    -> (string list * Bytes.T) list * string
   val compilation_text': Proof.context -> string -> string option -> Code_Thingol.program
     -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
-    -> ((string list * string) list * string) * (Code_Symbol.T -> string option)
+    -> ((string list * Bytes.T) list * string) * (Code_Symbol.T -> string option)
 
   type serializer
   type literals = Code_Printer.literals
@@ -289,7 +289,7 @@
 fun export binding content thy =
   let
     val thy' = thy |> Generated_Files.add_files (binding, content);
-    val _ = Export.export thy' binding [XML.Text content];
+    val _ = Export.export thy' binding (Bytes.contents_blob content);
   in thy' end;
 
 local
@@ -309,11 +309,11 @@
 
 fun export_physical root format pretty_modules =
   (case pretty_modules of
-    Singleton (_, p) => File.write root (format p)
+    Singleton (_, p) => Bytes.write root (format p)
   | Hierarchy code_modules =>
       (Isabelle_System.make_directory root;
         List.app (fn (names, p) =>
-          File.write (Path.appends (root :: map Path.basic names)) (format p)) code_modules));
+          Bytes.write (Path.appends (root :: map Path.basic names)) (format p)) code_modules));
 
 in
 
@@ -343,7 +343,8 @@
   let val format = Code_Printer.format selects width in
     (case pretty_modules of
       Singleton (_, p) => format p
-    | Hierarchy code_modules => space_implode "\n\n" (map (format o #2) code_modules))
+    | Hierarchy code_modules =>
+        Bytes.appends (separate (Bytes.string "\n\n") (map (format o #2) code_modules)))
   end;
 
 end;
@@ -788,6 +789,7 @@
     (fn ctxt => fn ((consts, symbols), (target_name, some_width)) =>
        present_code ctxt consts symbols
          target_name "Example" some_width []
+       |> Bytes.content
        |> trim_line
        |> Document_Output.verbatim (Config.put Document_Antiquotation.thy_output_display true ctxt)));