# HG changeset patch
# User wenzelm
# Date 1725993361 -7200
# Node ID df85df6315af372b513d5debd339705d495bd69c
# Parent  93c2058896a4edf927bd4e08840366339d796b79
clarified signature: prefer explicit type Bytes.T;

diff -r 93c2058896a4 -r df85df6315af src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Tue Sep 10 20:06:51 2024 +0200
+++ b/src/Pure/General/pretty.ML	Tue Sep 10 20:36:01 2024 +0200
@@ -73,13 +73,12 @@
     margin: int}
   val output_ops: int option -> output_ops
   val markup_output_ops: int option -> output_ops
-  val symbolic_output: T -> Output.output list
+  val symbolic_output: T -> Bytes.T
   val symbolic_string_of: T -> string
   val unformatted_string_of: T -> string
   val regularN: string
   val symbolicN: string
-  val output_buffer: output_ops -> T -> Buffer.T
-  val output: output_ops -> T -> Output.output list
+  val output: output_ops -> T -> Bytes.T
   val string_of_ops: output_ops -> T -> string
   val string_of: T -> string
   val writeln: T -> unit
@@ -251,6 +250,7 @@
 
 fun output_spaces (ops: output_ops) = #output ops o Symbol.spaces;
 fun output_spaces_buffer ops = Buffer.add o #1 o output_spaces ops;
+fun output_spaces_bytes ops = Bytes.add o #1 o output_spaces ops;
 
 
 (* output tree *)
@@ -315,28 +315,28 @@
 
 local
 
-type text = {tx: Buffer.T, ind: Buffer.T, pos: int, nl: int};
+type text = {tx: Bytes.T, ind: Buffer.T, pos: int, nl: int};
 
 val empty: text =
- {tx = Buffer.empty,
+ {tx = Bytes.empty,
   ind = Buffer.empty,
   pos = 0,
   nl = 0};
 
 fun newline s {tx, ind = _, pos = _, nl} : text =
- {tx = Buffer.add s tx,
+ {tx = Bytes.add s tx,
   ind = Buffer.empty,
   pos = 0,
   nl = nl + 1};
 
 fun control s {tx, ind, pos: int, nl} : text =
- {tx = Buffer.add s tx,
+ {tx = Bytes.add s tx,
   ind = ind,
   pos = pos,
   nl = nl};
 
 fun string (s, len) {tx, ind, pos: int, nl} : text =
- {tx = Buffer.add s tx,
+ {tx = Bytes.add s tx,
   ind = Buffer.add s ind,
   pos = pos + len,
   nl = nl};
@@ -369,7 +369,7 @@
 
     fun indentation (buf, len) {tx, ind, pos, nl} : text =
       let val s = Buffer.content buf in
-       {tx = Buffer.add (#indent ops s len) tx,
+       {tx = Bytes.add (#indent ops s len) tx,
         ind = Buffer.add s ind,
         pos = pos + len,
         nl = nl}
@@ -418,40 +418,39 @@
 
 (* symbolic output: XML markup for blocks/breaks + other markup *)
 
-val symbolic =
+val symbolic_output =
   let
     val ops = markup_output_ops NONE;
 
-    fun markup_buffer m body =
+    fun markup_bytes m body =
       let val (bg, en) = #markup ops (YXML.output_markup m)
-      in Buffer.add bg #> body #> Buffer.add en end;
+      in Bytes.add bg #> body #> Bytes.add en end;
 
-    fun out (Block ((bg, en), _, _, [], _)) = Buffer.add bg #> Buffer.add en
+    fun out (Block ((bg, en), _, _, [], _)) = Bytes.add bg #> Bytes.add en
       | out (Block ((bg, en), consistent, indent, prts, _)) =
-          Buffer.add bg #>
-          markup_buffer (Markup.block consistent indent) (fold out prts) #>
-          Buffer.add en
+          Bytes.add bg #>
+          markup_bytes (Markup.block consistent indent) (fold out prts) #>
+          Bytes.add en
       | out (Break (false, wd, ind)) =
-          markup_buffer (Markup.break wd ind) (output_spaces_buffer ops wd)
-      | out (Break (true, _, _)) = Buffer.add (output_newline ops)
-      | out (Str (s, _)) = Buffer.add s;
-  in Buffer.build o out o output_tree ops false end;
+          markup_bytes (Markup.break wd ind) (output_spaces_bytes ops wd)
+      | out (Break (true, _, _)) = Bytes.add (output_newline ops)
+      | out (Str (s, _)) = Bytes.add s;
+  in Bytes.build o out o output_tree ops false end;
 
-val symbolic_output = Buffer.contents o symbolic;
-val symbolic_string_of = implode o symbolic_output;
+val symbolic_string_of = Bytes.content o symbolic_output;
 
 
 (* unformatted output: other markup only *)
 
 fun unformatted ops =
   let
-    fun out (Block ((bg, en), _, _, prts, _)) = Buffer.add bg #> fold out prts #> Buffer.add en
-      | out (Break (_, wd, _)) = output_spaces_buffer ops wd
-      | out (Str (s, _)) = Buffer.add s;
-  in Buffer.build o out o output_tree ops false end;
+    fun out (Block ((bg, en), _, _, prts, _)) = Bytes.add bg #> fold out prts #> Bytes.add en
+      | out (Break (_, wd, _)) = output_spaces_bytes ops wd
+      | out (Str (s, _)) = Bytes.add s;
+  in Bytes.build o out o output_tree ops false end;
 
 fun unformatted_string_of prt =
-  Buffer.content (unformatted (output_ops NONE) prt);
+  Bytes.content (unformatted (output_ops NONE) prt);
 
 
 (* output interfaces *)
@@ -459,19 +458,16 @@
 val regularN = "pretty_regular";
 val symbolicN = "pretty_symbolic";
 
-fun output_buffer ops prt =
+fun output ops prt =
   if print_mode_active symbolicN andalso not (print_mode_active regularN)
-  then symbolic prt
+  then symbolic_output prt
   else format_tree ops prt;
 
-val output = Buffer.contents oo output_buffer;
-
-fun string_of_ops ops = implode o output ops;
+fun string_of_ops ops = Bytes.content o output ops;
 fun string_of prt = string_of_ops (output_ops NONE) prt;
 
 fun writeln prt =
-  let val ops = output_ops NONE
-  in Output.writelns (output ops prt) end;
+  Output.writelns (Bytes.contents (output (output_ops NONE) prt));
 
 
 (* chunks *)
diff -r 93c2058896a4 -r df85df6315af src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Tue Sep 10 20:06:51 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue Sep 10 20:36:01 2024 +0200
@@ -766,7 +766,7 @@
       if show_markup andalso not show_types then
         let
           val ((bg1, bg2), en) = typing_elem;
-          val bg = implode (bg1 :: Pretty.symbolic_output (pretty_typ_ast Markup.empty ty) @ [bg2]);
+          val bg = implode (bg1 :: symbolic_typ_ast ty @ [bg2]);
           val info = {markup = (bg, en), consistent = false, indent = 0};
         in SOME (Pretty.make_block info [pretty_ast Markup.empty t]) end
       else NONE
@@ -775,7 +775,7 @@
       if show_markup andalso not show_sorts then
         let
           val ((bg1, bg2), en) = sorting_elem;
-          val bg = implode (bg1 :: Pretty.symbolic_output (pretty_typ_ast Markup.empty s) @ [bg2]);
+          val bg = implode (bg1 :: symbolic_typ_ast s @ [bg2]);
           val info = {markup = (bg, en), consistent = false, indent = 0};
         in SOME (Pretty.make_block info [pretty_typ_ast Markup.empty ty]) end
       else NONE
@@ -786,7 +786,10 @@
 
     and pretty_ast m ast = ast
       |> prt_t ctxt prtabs trf markup_trans markup_extern
-      |> Pretty.markup m;
+      |> Pretty.markup m
+
+    and symbolic_typ_ast ast =
+      Bytes.contents (Pretty.symbolic_output (pretty_typ_ast Markup.empty ast));
   in
     t_to_ast ctxt (Syntax.print_translation syn) t
     |> Ast.normalize ctxt (Syntax.print_rules syn)
diff -r 93c2058896a4 -r df85df6315af src/Pure/Thy/document_antiquotation.ML
--- a/src/Pure/Thy/document_antiquotation.ML	Tue Sep 10 20:06:51 2024 +0200
+++ b/src/Pure/Thy/document_antiquotation.ML	Tue Sep 10 20:36:01 2024 +0200
@@ -86,7 +86,7 @@
   let
     val breakable = Config.get ctxt thy_output_display orelse Config.get ctxt thy_output_break;
     val ops = Latex.output_ops (SOME (Config.get ctxt thy_output_margin));
-  in not breakable ? Pretty.unbreakable #> Pretty.output ops #> implode #> Latex.escape end;
+  in not breakable ? Pretty.unbreakable #> Pretty.output ops #> Bytes.content #> Latex.escape end;
 
 fun output ctxt = delimit ctxt #> indent ctxt #> format ctxt #> Latex.output_;
 
diff -r 93c2058896a4 -r df85df6315af src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Tue Sep 10 20:06:51 2024 +0200
+++ b/src/Tools/Code/code_printer.ML	Tue Sep 10 20:36:01 2024 +0200
@@ -138,10 +138,10 @@
 fun markup_stmt sym =
   Pretty.mark (code_presentationN, [(stmt_nameN, Code_Symbol.marker sym)]);
 
-val add_text = XML.traverse_text Buffer.add;
+val add_text = XML.traverse_text Bytes.add;
 
 fun filter_presentation [] xml =
-      Buffer.build (fold add_text xml)
+      Bytes.build (fold add_text xml)
   | filter_presentation presentation_syms xml =
       let
         val presentation_idents = map Code_Symbol.marker presentation_syms
@@ -150,21 +150,19 @@
           andalso member (op =) presentation_idents (the (Properties.get attrs stmt_nameN));
         fun add_content_with_space tree (is_first, buf) =
           buf
-          |> not is_first ? Buffer.add "\n\n"
+          |> not is_first ? Bytes.add "\n\n"
           |> add_text tree
           |> pair false;
         fun filter (XML.Elem (name_attrs, xs)) =
               fold (if is_selected name_attrs then add_content_with_space else filter) xs
           | filter (XML.Text _) = I;
-      in snd (fold filter xml (true, Buffer.empty)) end;
+      in snd (fold filter xml (true, Bytes.empty)) end;
 
 fun format presentation_names width =
-  Pretty.output_buffer (Pretty.markup_output_ops (SOME width))
-  #> Bytes.buffer
+  Pretty.output (Pretty.markup_output_ops (SOME width))
   #> YXML.parse_body_bytes
   #> filter_presentation presentation_names
-  #> Buffer.add "\n"
-  #> Bytes.buffer;
+  #> Bytes.add "\n";
 
 
 (** names and variable name contexts **)