--- a/src/HOL/Library/code_test.ML Wed Jun 22 08:15:14 2022 +0000
+++ b/src/HOL/Library/code_test.ML Thu Jun 23 22:16:53 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 Wed Jun 22 08:15:14 2022 +0000
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Jun 23 22:16:53 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/bytes.ML Wed Jun 22 08:15:14 2022 +0000
+++ b/src/Pure/General/bytes.ML Thu Jun 23 22:16:53 2022 +0200
@@ -12,6 +12,7 @@
sig
val chunk_size: int
type T
+ val eq: T * T -> bool
val length: T -> int
val contents: T -> string list
val contents_blob: T -> XML.body
@@ -27,6 +28,7 @@
val last_string: T -> string option
val trim_line: T -> T
val append: T -> T -> T
+ val appends: T list -> T
val string: string -> T
val newline: T
val buffer: Buffer.T -> T
@@ -56,6 +58,10 @@
val compact = implode o rev;
+fun eq (Bytes {buffer, chunks, m, n}, Bytes {buffer = buffer', chunks = chunks', m = m', n = n'}) =
+ m = m' andalso n = n' andalso chunks = chunks' andalso
+ (buffer = buffer' orelse compact buffer = compact buffer);
+
fun contents (Bytes {buffer, chunks, ...}) =
rev (chunks |> not (null buffer) ? cons (compact buffer));
@@ -136,6 +142,8 @@
else if is_empty bytes2 then bytes1
else bytes1 |> fold add (contents bytes2);
+val appends = build o fold (fn b => fn a => append a b);
+
val string = build o add;
val newline = string "\n";
@@ -196,10 +204,12 @@
| s => read (add s bytes))
in read empty end;
-fun write_stream stream = File.outputs stream o contents;
+fun write_stream stream bytes =
+ File.outputs stream (contents bytes);
-val read = File.open_input (read_stream ~1);
-val write = File.open_output write_stream;
+fun read path = File.open_input (fn stream => read_stream ~1 stream) path;
+
+fun write path bytes = File.open_output (fn stream => write_stream stream bytes) path;
(* ML pretty printing *)
--- a/src/Pure/General/file.ML Wed Jun 22 08:15:14 2022 +0000
+++ b/src/Pure/General/file.ML Thu Jun 23 22:16:53 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 Wed Jun 22 08:15:14 2022 +0000
+++ b/src/Pure/Thy/export.ML Thu Jun 23 22:16:53 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 Wed Jun 22 08:15:14 2022 +0000
+++ b/src/Pure/Tools/generated_files.ML Thu Jun 23 22:16:53 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 Wed Jun 22 08:15:14 2022 +0000
+++ b/src/Tools/Code/code_printer.ML Thu Jun 23 22:16:53 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 Wed Jun 22 08:15:14 2022 +0000
+++ b/src/Tools/Code/code_runtime.ML Thu Jun 23 22:16:53 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 Wed Jun 22 08:15:14 2022 +0000
+++ b/src/Tools/Code/code_target.ML Thu Jun 23 22:16:53 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)));