# HG changeset patch
# User desharna
# Date 1656098255 -7200
# Node ID da901dcafc2952be3709c60f102b1567c3f28daf
# Parent  19ec8f844e08fc0d8baf71512249399e67268d57# Parent  0f7cb6cd08fe6d1eaa695794e76f0e576c13660e
merged

diff -r 19ec8f844e08 -r da901dcafc29 NEWS
--- a/NEWS	Fri Jun 24 10:49:40 2022 +0200
+++ b/NEWS	Fri Jun 24 21:17:35 2022 +0200
@@ -34,6 +34,9 @@
 
 *** HOL ***
 
+* Theory Char_ord: streamlined logical specifications.
+Minor INCOMPATIBILITY.
+
 * Rule split_of_bool_asm is not split any longer, analogously to
 split_if_asm.  INCOMPATIBILITY.
 
diff -r 19ec8f844e08 -r da901dcafc29 src/HOL/Library/Char_ord.thy
--- a/src/HOL/Library/Char_ord.thy	Fri Jun 24 10:49:40 2022 +0200
+++ b/src/HOL/Library/Char_ord.thy	Fri Jun 24 21:17:35 2022 +0200
@@ -8,14 +8,93 @@
   imports Main
 begin
 
+context linordered_semidom
+begin
+
+lemma horner_sum_nonnegative:
+  \<open>0 \<le> horner_sum of_bool 2 bs\<close>
+  by (induction bs) simp_all
+
+end
+
+context unique_euclidean_semiring_numeral
+begin
+
+lemma horner_sum_bound:
+  \<open>horner_sum of_bool 2 bs < 2 ^ length bs\<close>
+proof (induction bs)
+  case Nil
+  then show ?case
+    by simp
+next
+  case (Cons b bs)
+  moreover define a where \<open>a = 2 ^ length bs - horner_sum of_bool 2 bs\<close>
+  ultimately have *: \<open>2 ^ length bs = horner_sum of_bool 2 bs + a\<close>
+    by simp
+  have \<open>1 < a * 2\<close> if \<open>0 < a\<close>
+    using that add_mono [of 1 a 1 a]
+    by (simp add: mult_2_right discrete)
+  with Cons show ?case
+    by (simp add: algebra_simps *)
+qed
+
+end
+
+context unique_euclidean_semiring_numeral
+begin
+
+lemma horner_sum_less_eq_iff_lexordp_eq:
+  \<open>horner_sum of_bool 2 bs \<le> horner_sum of_bool 2 cs \<longleftrightarrow> lexordp_eq (rev bs) (rev cs)\<close>
+  if \<open>length bs = length cs\<close>
+proof -
+  have \<open>horner_sum of_bool 2 (rev bs) \<le> horner_sum of_bool 2 (rev cs) \<longleftrightarrow> lexordp_eq bs cs\<close>
+    if \<open>length bs = length cs\<close> for bs cs
+  using that proof (induction bs cs rule: list_induct2)
+    case Nil
+    then show ?case
+      by simp
+  next
+    case (Cons b bs c cs)
+    with horner_sum_nonnegative [of \<open>rev bs\<close>] horner_sum_nonnegative [of \<open>rev cs\<close>]
+      horner_sum_bound [of \<open>rev bs\<close>] horner_sum_bound [of \<open>rev cs\<close>]
+    show ?case
+      by (auto simp add: horner_sum_append not_le Cons intro: add_strict_increasing2 add_increasing)
+  qed
+  from that this [of \<open>rev bs\<close> \<open>rev cs\<close>] show ?thesis
+    by simp
+qed
+
+lemma horner_sum_less_iff_lexordp:
+  \<open>horner_sum of_bool 2 bs < horner_sum of_bool 2 cs \<longleftrightarrow> ord_class.lexordp (rev bs) (rev cs)\<close>
+  if \<open>length bs = length cs\<close>
+proof -
+  have \<open>horner_sum of_bool 2 (rev bs) < horner_sum of_bool 2 (rev cs) \<longleftrightarrow> ord_class.lexordp bs cs\<close>
+    if \<open>length bs = length cs\<close> for bs cs
+  using that proof (induction bs cs rule: list_induct2)
+    case Nil
+    then show ?case
+      by simp
+  next
+    case (Cons b bs c cs)
+    with horner_sum_nonnegative [of \<open>rev bs\<close>] horner_sum_nonnegative [of \<open>rev cs\<close>]
+      horner_sum_bound [of \<open>rev bs\<close>] horner_sum_bound [of \<open>rev cs\<close>]
+    show ?case
+      by (auto simp add: horner_sum_append not_less Cons intro: add_strict_increasing2 add_increasing)
+  qed
+  from that this [of \<open>rev bs\<close> \<open>rev cs\<close>] show ?thesis
+    by simp
+qed
+
+end
+
 instantiation char :: linorder
 begin
 
-definition less_eq_char :: "char \<Rightarrow> char \<Rightarrow> bool"
-  where "c1 \<le> c2 \<longleftrightarrow> of_char c1 \<le> (of_char c2 :: nat)"
+definition less_eq_char :: \<open>char \<Rightarrow> char \<Rightarrow> bool\<close>
+  where \<open>c1 \<le> c2 \<longleftrightarrow> of_char c1 \<le> (of_char c2 :: nat)\<close>
 
-definition less_char :: "char \<Rightarrow> char \<Rightarrow> bool"
-  where "c1 < c2 \<longleftrightarrow> of_char c1 < (of_char c2 :: nat)"
+definition less_char :: \<open>char \<Rightarrow> char \<Rightarrow> bool\<close>
+  where \<open>c1 < c2 \<longleftrightarrow> of_char c1 < (of_char c2 :: nat)\<close>
 
 
 instance
@@ -23,23 +102,21 @@
 
 end
 
-lemma less_eq_char_simp [simp]:
-  "Char b0 b1 b2 b3 b4 b5 b6 b7 \<le> Char c0 c1 c2 c3 c4 c5 c6 c7
-    \<longleftrightarrow> foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0
-      \<le> foldr (\<lambda>b k. of_bool b + k * 2) [c0, c1, c2, c3, c4, c5, c6, c7] (0::nat)"
-  by (simp add: less_eq_char_def)
+lemma less_eq_char_simp [simp, code]:
+  \<open>Char b0 b1 b2 b3 b4 b5 b6 b7 \<le> Char c0 c1 c2 c3 c4 c5 c6 c7
+    \<longleftrightarrow> lexordp_eq [b7, b6, b5, b4, b3, b2, b1, b0] [c7, c6, c5, c4, c3, c2, c1, c0]\<close>
+  by (simp only: less_eq_char_def of_char_def char.sel horner_sum_less_eq_iff_lexordp_eq list.size) simp
 
-lemma less_char_simp [simp]:
-  "Char b0 b1 b2 b3 b4 b5 b6 b7 < Char c0 c1 c2 c3 c4 c5 c6 c7
-    \<longleftrightarrow> foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0
-      < foldr (\<lambda>b k. of_bool b + k * 2) [c0, c1, c2, c3, c4, c5, c6, c7] (0::nat)"
-  by (simp add: less_char_def)
+lemma less_char_simp [simp, code]:
+  \<open>Char b0 b1 b2 b3 b4 b5 b6 b7 < Char c0 c1 c2 c3 c4 c5 c6 c7
+    \<longleftrightarrow> ord_class.lexordp [b7, b6, b5, b4, b3, b2, b1, b0] [c7, c6, c5, c4, c3, c2, c1, c0]\<close>
+  by (simp only: less_char_def of_char_def char.sel horner_sum_less_iff_lexordp list.size) simp
 
 instantiation char :: distrib_lattice
 begin
 
-definition "(inf :: char \<Rightarrow> _) = min"
-definition "(sup :: char \<Rightarrow> _) = max"
+definition \<open>(inf :: char \<Rightarrow> _) = min\<close>
+definition \<open>(sup :: char \<Rightarrow> _) = max\<close>
 
 instance
   by standard (auto simp add: inf_char_def sup_char_def max_min_distrib2)
diff -r 19ec8f844e08 -r da901dcafc29 src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Fri Jun 24 10:49:40 2022 +0200
+++ b/src/HOL/Library/code_test.ML	Fri Jun 24 21:17:35 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
diff -r 19ec8f844e08 -r da901dcafc29 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Jun 24 10:49:40 2022 +0200
+++ b/src/HOL/List.thy	Fri Jun 24 21:17:35 2022 +0200
@@ -2247,13 +2247,13 @@
 
 lemma butlast_take:
   "n \<le> length xs \<Longrightarrow> butlast (take n xs) = take (n - 1) xs"
-  by (simp add: butlast_conv_take min.absorb1 min.absorb2)
+  by (simp add: butlast_conv_take)
 
 lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
   by (simp add: butlast_conv_take drop_take ac_simps)
 
 lemma take_butlast: "n < length xs \<Longrightarrow> take n (butlast xs) = take n xs"
-  by (simp add: butlast_conv_take min.absorb1)
+  by (simp add: butlast_conv_take)
 
 lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
   by (simp add: butlast_conv_take drop_take ac_simps)
@@ -2374,7 +2374,7 @@
 qed auto
 
 lemma nth_image: "l \<le> size xs \<Longrightarrow> nth xs ` {0..<l} = set(take l xs)"
-  by(auto simp: set_conv_nth image_def) (metis Suc_le_eq nth_take order_trans)
+  by (simp add: set_conv_nth) force
 
 
 subsubsection \<open>\<^const>\<open>takeWhile\<close> and \<^const>\<open>dropWhile\<close>\<close>
@@ -2808,7 +2808,7 @@
     proof (induction "zip xs (zip ys zs)" arbitrary: xs ys zs)
       case Nil
       from Nil [symmetric] show ?case
-        by (auto simp add: zip_eq_Nil_iff)
+        by auto
     next
       case (Cons xyz xyzs)
       from Cons.hyps(2) [symmetric] show ?case
@@ -2820,7 +2820,7 @@
     proof (induction "zip xs ys" arbitrary: xs ys)
       case Nil
       then show ?case
-        by (auto simp add: zip_eq_Nil_iff dest: sym)
+        by auto
     next
       case (Cons xy xys)
       from Cons.hyps(2) [symmetric] show ?case
@@ -3702,8 +3702,9 @@
 proof (induct xs)
   case (Cons x xs)
   show ?case
-    apply (auto simp add: Cons nth_Cons split: nat.split_asm)
-    apply (metis Suc_less_eq2 in_set_conv_nth less_not_refl zero_less_Suc)+
+    apply (auto simp add: Cons nth_Cons less_Suc_eq_le split: nat.split_asm)
+    apply (metis Suc_leI in_set_conv_nth length_pos_if_in_set lessI less_imp_le_nat less_nat_zero_code)
+    apply (metis Suc_le_eq)
     done
 qed auto
 
@@ -5256,8 +5257,8 @@
     case (Suc j)
     have *: "\<And>xss. xs # map tl xss = map tl ((x#xs)#xss)" by simp
     have **: "\<And>xss. (x#xs) # filter (\<lambda>ys. ys \<noteq> []) xss = filter (\<lambda>ys. ys \<noteq> []) ((x#xs)#xss)" by simp
-    { fix x have "Suc j < length x \<longleftrightarrow> x \<noteq> [] \<and> j < length x - Suc 0"
-      by (cases x) simp_all
+    { fix xs :: \<open>'a list\<close> have "Suc j < length xs \<longleftrightarrow> xs \<noteq> [] \<and> j < length xs - Suc 0"
+      by (cases xs) simp_all
     } note *** = this
 
     have j_less: "j < length (transpose (xs # concat (map (case_list [] (\<lambda>h t. [t])) xss)))"
@@ -5282,6 +5283,7 @@
     by (simp add: nth_transpose filter_map comp_def)
 qed
 
+
 subsubsection \<open>\<^const>\<open>min\<close> and \<^const>\<open>arg_min\<close>\<close>
 
 lemma min_list_Min: "xs \<noteq> [] \<Longrightarrow> min_list xs = Min (set xs)"
@@ -5548,8 +5550,6 @@
 
 lemmas sorted2_simps = sorted1 sorted2
 
-lemmas [code] = sorted0 sorted2_simps
-
 lemma sorted_append:
   "sorted (xs@ys) = (sorted xs \<and> sorted ys \<and> (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
 by (simp add: sorted_wrt_append)
@@ -5966,6 +5966,9 @@
 lemma sorted_enumerate [simp]: "sorted (map fst (enumerate n xs))"
 by (simp add: enumerate_eq_zip)
 
+lemma sorted_insort_is_snoc: "sorted xs \<Longrightarrow> \<forall>x \<in> set xs. a \<ge> x \<Longrightarrow> insort a xs = xs @ [a]"
+ by (induct xs) (auto dest!: insort_is_Cons)
+
 text \<open>Stability of \<^const>\<open>sort_key\<close>:\<close>
 
 lemma sort_key_stable: "filter (\<lambda>y. f y = k) (sort_key f xs) = filter (\<lambda>y. f y = k) xs"
@@ -7011,7 +7014,7 @@
 
 end
 
-lemma lexordp_simps [simp]:
+lemma lexordp_simps [simp, code]:
   "lexordp [] ys = (ys \<noteq> [])"
   "lexordp xs [] = False"
   "lexordp (x # xs) (y # ys) \<longleftrightarrow> x < y \<or> \<not> y < x \<and> lexordp xs ys"
@@ -7022,7 +7025,7 @@
 | Cons: "x < y \<Longrightarrow> lexordp_eq (x # xs) (y # ys)"
 | Cons_eq: "\<lbrakk> \<not> x < y; \<not> y < x; lexordp_eq xs ys \<rbrakk> \<Longrightarrow> lexordp_eq (x # xs) (y # ys)"
 
-lemma lexordp_eq_simps [simp]:
+lemma lexordp_eq_simps [simp, code]:
   "lexordp_eq [] ys = True"
   "lexordp_eq xs [] \<longleftrightarrow> xs = []"
   "lexordp_eq (x # xs) [] = False"
@@ -7062,7 +7065,7 @@
 end
 
 declare ord.lexordp_simps [simp, code]
-declare ord.lexordp_eq_simps [code, simp]
+declare ord.lexordp_eq_simps [simp, code]
 
 context order
 begin
@@ -7155,9 +7158,6 @@
 
 end
 
-lemma sorted_insort_is_snoc: "sorted xs \<Longrightarrow> \<forall>x \<in> set xs. a \<ge> x \<Longrightarrow> insort a xs = xs @ [a]"
- by (induct xs) (auto dest!: insort_is_Cons)
-
 
 subsubsection \<open>Lexicographic combination of measure functions\<close>
 
diff -r 19ec8f844e08 -r da901dcafc29 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Jun 24 10:49:40 2022 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Jun 24 21:17:35 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 ()
diff -r 19ec8f844e08 -r da901dcafc29 src/Pure/General/bytes.ML
--- a/src/Pure/General/bytes.ML	Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Pure/General/bytes.ML	Fri Jun 24 21:17:35 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,9 +28,14 @@
   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
+  val space_explode: string -> T -> string list
+  val split_lines: T -> string list
+  val trim_split_lines: T -> string list
+  val cat_lines: string list -> T
   val read_block: int -> BinIO.instream -> string
   val read_stream: int -> BinIO.instream -> T
   val write_stream: BinIO.outstream -> T -> unit
@@ -52,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));
 
@@ -132,12 +142,57 @@
   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";
 
 val buffer = build o fold add o Buffer.contents;
 
+
+(* space_explode *)
+
+fun space_explode sep bytes =
+  if is_empty bytes then []
+  else if size sep <> 1 then [content bytes]
+  else
+    let
+      val sep_char = String.sub (sep, 0);
+
+      fun add_part s part =
+        Buffer.add (Substring.string s) (the_default Buffer.empty part);
+
+      fun explode head tail part res =
+        if Substring.isEmpty head then
+          (case tail of
+            [] =>
+              (case part of
+                NONE => rev res
+              | SOME buf => rev (Buffer.content buf :: res))
+          | chunk :: chunks => explode (Substring.full chunk) chunks part res)
+        else
+          (case Substring.fields (fn c => c = sep_char) head of
+            [a] => explode Substring.empty tail (SOME (add_part a part)) res
+          | a :: rest =>
+              let
+                val (bs, c) = split_last rest;
+                val res' = res
+                  |> cons (Buffer.content (add_part a part))
+                  |> fold (cons o Substring.string) bs;
+                val part' = SOME (add_part c NONE);
+              in explode Substring.empty tail part' res' end)
+    in explode Substring.empty (contents bytes) NONE [] end;
+
+val split_lines = space_explode "\n";
+
+val trim_split_lines = trim_line #> split_lines #> map Library.trim_line;
+
+fun cat_lines lines = build (fold add (separate "\n" lines));
+
+
+(* IO *)
+
 fun read_block limit =
   File.input_size (if limit < 0 then chunk_size else Int.min (chunk_size, limit));
 
@@ -149,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 *)
diff -r 19ec8f844e08 -r da901dcafc29 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Pure/General/bytes.scala	Fri Jun 24 21:17:35 2022 +0200
@@ -42,36 +42,32 @@
 
   /* base64 */
 
-  def base64(s: String): Bytes = {
+  def decode_base64(s: String): Bytes = {
     val a = Base64.getDecoder.decode(s)
     new Bytes(a, 0, a.length)
   }
 
-  object Decode_Base64 extends Scala.Fun("decode_base64") {
+  object Decode_Base64 extends Scala.Fun_Bytes("decode_base64") {
     val here = Scala_Project.here
-    def invoke(args: List[Bytes]): List[Bytes] =
-      List(base64(Library.the_single(args).text))
+    def apply(arg: Bytes): Bytes = decode_base64(arg.text)
   }
 
-  object Encode_Base64 extends Scala.Fun("encode_base64") {
+  object Encode_Base64 extends Scala.Fun_Bytes("encode_base64") {
     val here = Scala_Project.here
-    def invoke(args: List[Bytes]): List[Bytes] =
-      List(Bytes(Library.the_single(args).base64))
+    def apply(arg: Bytes): Bytes = Bytes(arg.encode_base64)
   }
 
 
   /* XZ compression */
 
-  object Compress extends Scala.Fun("compress") {
+  object Compress extends Scala.Fun_Bytes("compress") {
     val here = Scala_Project.here
-    def invoke(args: List[Bytes]): List[Bytes] =
-      List(Library.the_single(args).compress())
+    def apply(arg: Bytes): Bytes = arg.compress()
   }
 
-  object Uncompress extends Scala.Fun("uncompress") {
+  object Uncompress extends Scala.Fun_Bytes("uncompress") {
     val here = Scala_Project.here
-    def invoke(args: List[Bytes]): List[Bytes] =
-      List(Library.the_single(args).uncompress())
+    def apply(arg: Bytes): Bytes = arg.uncompress()
   }
 
 
@@ -160,16 +156,16 @@
 
   def text: String = UTF8.decode_permissive(this)
 
-  def base64: String = {
+  def encode_base64: String = {
     val b =
       if (offset == 0 && length == bytes.length) bytes
       else Bytes(bytes, offset, length).bytes
     Base64.getEncoder.encodeToString(b)
   }
 
-  def maybe_base64: (Boolean, String) = {
+  def maybe_encode_base64: (Boolean, String) = {
     val s = text
-    if (this == Bytes(s)) (false, s) else (true, base64)
+    if (this == Bytes(s)) (false, s) else (true, encode_base64)
   }
 
   override def toString: String = "Bytes(" + length + ")"
diff -r 19ec8f844e08 -r da901dcafc29 src/Pure/General/csv.scala
--- a/src/Pure/General/csv.scala	Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Pure/General/csv.scala	Fri Jun 24 21:17:35 2022 +0200
@@ -10,7 +10,7 @@
 object CSV {
   def print_field(field: Any): String = {
     val str = field.toString
-    if (str.exists("\",\r\n".contains(_))) {
+    if (str.exists("\",\r\n ".contains(_))) {
       (for (c <- str) yield { if (c == '"') "\"\"" else c.toString }).mkString("\"", "", "\"")
     }
     else str
diff -r 19ec8f844e08 -r da901dcafc29 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Pure/General/file.ML	Fri Jun 24 21:17:35 2022 +0200
@@ -30,13 +30,10 @@
   val input_size: int -> BinIO.instream -> string
   val input_all: BinIO.instream -> string
   val fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
-  val fold_pages: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
   val read_lines: Path.T -> string list
-  val read_pages: Path.T -> string list
   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
@@ -143,24 +140,20 @@
   . avoid size limit of TextIO.inputAll and overhead of many TextIO.inputLine
   . optional terminator at end-of-input
 *)
-fun fold_chunks terminator f path a = open_input (fn file =>
+fun fold_lines f path a = open_input (fn file =>
   let
     fun read buf x =
       (case input file of
         "" => (case Buffer.content buf of "" => x | line => f line x)
       | input =>
-          (case String.fields (fn c => c = terminator) input of
+          (case String.fields (fn c => c = #"\n") input of
             [rest] => read (Buffer.add rest buf) x
-          | line :: more => read_lines more (f (Buffer.content (Buffer.add line buf)) x)))
-    and read_lines [rest] x = read (Buffer.add rest Buffer.empty) x
-      | read_lines (line :: more) x = read_lines more (f line x);
+          | line :: more => read_more more (f (Buffer.content (Buffer.add line buf)) x)))
+    and read_more [rest] x = read (Buffer.add rest Buffer.empty) x
+      | read_more (line :: more) x = read_more more (f line x);
   in read Buffer.empty a end) path;
 
-fun fold_lines f = fold_chunks #"\n" f;
-fun fold_pages f = fold_chunks #"\f" f;
-
 fun read_lines path = rev (fold_lines cons path []);
-fun read_pages path = rev (fold_pages cons path []);
 
 val read = open_input input_all;
 
@@ -176,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;
diff -r 19ec8f844e08 -r da901dcafc29 src/Pure/ML/ml_init.ML
--- a/src/Pure/ML/ml_init.ML	Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Pure/ML/ml_init.ML	Fri Jun 24 21:17:35 2022 +0200
@@ -33,3 +33,9 @@
     if n = 1 then String.str (String.sub (s, i))
     else String.substring (s, i, n);
 end;
+
+structure Substring =
+struct
+  open Substring;
+  val empty = full "";
+end;
diff -r 19ec8f844e08 -r da901dcafc29 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Pure/ML/ml_process.scala	Fri Jun 24 21:17:35 2022 +0200
@@ -72,22 +72,20 @@
 
 
     // options
+    val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
     val isabelle_process_options = Isabelle_System.tmp_file("options")
     Isabelle_System.chmod("600", File.path(isabelle_process_options))
     File.write(isabelle_process_options, YXML.string_of_body(options.encode))
-    val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
 
     // session base
+    val (init_session_base, eval_init_session) =
+      session_base match {
+        case None => (sessions_structure.bootstrap, Nil)
+        case Some(base) => (base, List("Resources.init_session_env ()"))
+      }
     val init_session = Isabelle_System.tmp_file("init_session")
     Isabelle_System.chmod("600", File.path(init_session))
-    val eval_init_session =
-      session_base match {
-        case None => Nil
-        case Some(base) =>
-          File.write(init_session, new Resources(sessions_structure, base).init_session_yxml)
-          List("Resources.init_session_file (Path.explode " +
-            ML_Syntax.print_string_bytes(File.path(init_session).implode) + ")")
-      }
+    File.write(init_session, new Resources(sessions_structure, init_session_base).init_session_yxml)
 
     // process
     val eval_process =
@@ -119,9 +117,9 @@
 
     val bash_env = new HashMap(env)
     bash_env.put("ISABELLE_PROCESS_OPTIONS", File.standard_path(isabelle_process_options))
+    bash_env.put("ISABELLE_INIT_SESSION", File.standard_path(init_session))
     bash_env.put("ISABELLE_TMP", File.standard_path(isabelle_tmp))
     bash_env.put("POLYSTATSDIR", isabelle_tmp.getAbsolutePath)
-    bash_env.put("ISABELLE_SCALA_FUNCTIONS", Scala.functions.mkString(","))
 
     Bash.process(
       options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
diff -r 19ec8f844e08 -r da901dcafc29 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Pure/PIDE/resources.ML	Fri Jun 24 21:17:35 2022 +0200
@@ -13,19 +13,18 @@
      bibtex_entries: (string * string list) list,
      command_timings: Properties.T list,
      load_commands: (string * Position.T) list,
-     scala_functions: (string * (bool * Position.T)) list,
+     scala_functions: (string * ((bool * bool) * Position.T)) list,
      global_theories: (string * string) list,
      loaded_theories: string list} -> unit
   val init_session_yxml: string -> unit
-  val init_session_file: Path.T -> unit
+  val init_session_env: unit -> unit
   val finish_session_base: unit -> unit
   val global_theory: string -> string option
   val loaded_theory: string -> bool
   val check_session: Proof.context -> string * Position.T -> string
   val last_timing: Toplevel.transition -> Time.time
   val check_load_command: Proof.context -> string * Position.T -> string
-  val scala_functions: unit -> string list
-  val check_scala_function: Proof.context -> string * Position.T -> string * bool
+  val check_scala_function: Proof.context -> string * Position.T -> string * (bool * bool)
   val master_directory: theory -> Path.T
   val imports_of: theory -> (string * Position.T) list
   val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
@@ -104,7 +103,7 @@
     bibtex_entries = Symtab.empty: string list Symtab.table,
     timings = empty_timings,
     load_commands = []: (string * Position.T) list,
-    scala_functions = Symtab.empty: (bool * Position.T) Symtab.table},
+    scala_functions = Symtab.empty: ((bool * bool) * Position.T) Symtab.table},
    {global_theories = Symtab.empty: string Symtab.table,
     loaded_theories = Symtab.empty: unit Symtab.table});
 
@@ -137,7 +136,7 @@
             (pair (list (pair string string))
               (pair (list (pair string (list string))) (pair (list properties)
                 (pair (list (pair string properties))
-                  (pair (list (pair string (pair bool properties)))
+                  (pair (list (pair string (pair (pair bool bool) properties)))
                     (pair (list (pair string string)) (list string))))))))
         end;
   in
@@ -152,8 +151,14 @@
        loaded_theories = loaded_theories}
   end;
 
-fun init_session_file path =
-  init_session_yxml (File.read path) before File.rm path;
+fun init_session_env () =
+  (case getenv "ISABELLE_INIT_SESSION" of
+    "" => ()
+  | name =>
+      try File.read (Path.explode name)
+      |> Option.app init_session_yxml);
+
+val _ = init_session_env ();
 
 fun finish_session_base () =
   Synchronized.change global_session_base
@@ -180,22 +185,13 @@
 
 (* Scala functions *)
 
-(*raw bootstrap environment*)
-fun scala_functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS");
-
-(*regular resources*)
-fun scala_function a =
-  (a, the_default (false, Position.none) (Symtab.lookup (get_session_base1 #scala_functions) a));
-
 fun check_scala_function ctxt arg =
   let
-    val funs = scala_functions () |> sort_strings |> map scala_function;
-    val name = Completion.check_entity Markup.scala_functionN (map (apsnd #2) funs) ctxt arg;
-    val multi =
-      (case AList.lookup (op =) funs name of
-        SOME (multi, _) => multi
-      | NONE => false);
-  in (name, multi) end;
+    val table = get_session_base1 #scala_functions;
+    val funs = Symtab.fold (fn (a, (_, pos)) => cons (a, pos)) table [] |> sort_by #1;
+    val name = Completion.check_entity Markup.scala_functionN funs ctxt arg;
+    val flags = #1 (the (Symtab.lookup table name));
+  in (name, flags) end;
 
 val _ = Theory.setup
  (Document_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_function\<close>
@@ -206,8 +202,10 @@
   ML_Antiquotation.value_embedded \<^binding>\<open>scala\<close>
     (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, arg) =>
       let
-        val (name, multi) = check_scala_function ctxt arg;
-        val func = if multi then "Scala.function" else "Scala.function1";
+        val (name, (single, bytes)) = check_scala_function ctxt arg;
+        val func =
+          (if single then "Scala.function1" else "Scala.function") ^
+          (if bytes then "_bytes" else "");
       in ML_Syntax.atomic (func ^ " " ^ ML_Syntax.print_string name) end)));
 
 
diff -r 19ec8f844e08 -r da901dcafc29 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Pure/PIDE/resources.scala	Fri Jun 24 21:17:35 2022 +0200
@@ -46,14 +46,14 @@
       pair(list(pair(string, list(string))),
       pair(list(properties),
       pair(list(pair(string, properties)),
-      pair(list(pair(string, pair(bool, properties))),
+      pair(list(Scala.encode_fun),
       pair(list(pair(string, string)), list(string))))))))(
        (sessions_structure.session_positions,
        (sessions_structure.dest_session_directories,
        (sessions_structure.bibtex_entries,
        (command_timings,
        (Command_Span.load_commands.map(cmd => (cmd.name, cmd.position)),
-       (Scala.functions.map(fun => (fun.name, (fun.multi, fun.position))),
+       (Scala.functions,
        (session_base.global_theories.toList,
         session_base.loaded_theories.keys)))))))))
   }
diff -r 19ec8f844e08 -r da901dcafc29 src/Pure/System/options.ML
--- a/src/Pure/System/options.ML	Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Pure/System/options.ML	Fri Jun 24 21:17:35 2022 +0200
@@ -211,11 +211,8 @@
   (case getenv "ISABELLE_PROCESS_OPTIONS" of
     "" => ()
   | name =>
-      let val path = Path.explode name in
-        (case try File.read path of
-          SOME s => set_default (decode (YXML.parse_body s))
-        | NONE => ())
-      end);
+      try File.read (Path.explode name)
+      |> Option.app (set_default o decode o YXML.parse_body));
 
 val _ = load_default ();
 val _ = ML_Print_Depth.set_print_depth (default_int "ML_print_depth");
diff -r 19ec8f844e08 -r da901dcafc29 src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Pure/System/scala.scala	Fri Jun 24 21:17:35 2022 +0200
@@ -18,12 +18,16 @@
 
   abstract class Fun(val name: String, val thread: Boolean = false) {
     override def toString: String = name
-    def multi: Boolean = true
+    def single: Boolean = false
+    def bytes: Boolean = false
     def position: Properties.T = here.position
     def here: Scala_Project.Here
     def invoke(args: List[Bytes]): List[Bytes]
   }
 
+  trait Single_Fun extends Fun { override def single: Boolean = true }
+  trait Bytes_Fun extends Fun { override def bytes: Boolean = true }
+
   abstract class Fun_Strings(name: String, thread: Boolean = false)
   extends Fun(name, thread = thread) {
     override def invoke(args: List[Bytes]): List[Bytes] =
@@ -32,13 +36,25 @@
   }
 
   abstract class Fun_String(name: String, thread: Boolean = false)
-  extends Fun_Strings(name, thread = thread) {
-    override def multi: Boolean = false
+  extends Fun_Strings(name, thread = thread) with Single_Fun {
     override def apply(args: List[String]): List[String] =
       List(apply(Library.the_single(args)))
     def apply(arg: String): String
   }
 
+  abstract class Fun_Bytes(name: String, thread: Boolean = false)
+    extends Fun(name, thread = thread) with Single_Fun with Bytes_Fun {
+    override def invoke(args: List[Bytes]): List[Bytes] =
+      List(apply(Library.the_single(args)))
+    def apply(arg: Bytes): Bytes
+  }
+
+  val encode_fun: XML.Encode.T[Fun] = { fun =>
+    import XML.Encode._
+    pair(string, pair(pair(bool, bool), properties))(
+      fun.name, ((fun.single, fun.bytes), fun.position))
+  }
+
   class Functions(val functions: Fun*) extends Isabelle_System.Service
 
   lazy val functions: List[Fun] =
diff -r 19ec8f844e08 -r da901dcafc29 src/Pure/Thy/export.ML
--- a/src/Pure/Thy/export.ML	Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Pure/Thy/export.ML	Fri Jun 24 21:17:35 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 *)
diff -r 19ec8f844e08 -r da901dcafc29 src/Pure/Tools/generated_files.ML
--- a/src/Pure/Tools/generated_files.ML	Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Pure/Tools/generated_files.ML	Fri Jun 24 21:17:35 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 ()
diff -r 19ec8f844e08 -r da901dcafc29 src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Pure/Tools/server_commands.scala	Fri Jun 24 21:17:35 2022 +0200
@@ -266,7 +266,7 @@
                     val matcher = Export.make_matcher(args.export_pattern)
                     for { entry <- snapshot.exports if matcher(entry.theory_name, entry.name) }
                     yield {
-                      val (base64, body) = entry.uncompressed.maybe_base64
+                      val (base64, body) = entry.uncompressed.maybe_encode_base64
                       JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body)
                     }
                   }))
diff -r 19ec8f844e08 -r da901dcafc29 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Tools/Code/code_printer.ML	Fri Jun 24 21:17:35 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 **)
diff -r 19ec8f844e08 -r da901dcafc29 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Tools/Code/code_runtime.ML	Fri Jun 24 21:17:35 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;
 
diff -r 19ec8f844e08 -r da901dcafc29 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Fri Jun 24 10:49:40 2022 +0200
+++ b/src/Tools/Code/code_target.ML	Fri Jun 24 21:17:35 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)));