more scalable pretty printing: avoid exception String.Size at command "value" (line 33 of "$AFP/Iptables_Semantics/Examples/SQRL_Shorewall/Analyze_SQRL_Shorewall.thy") in AFP/c69af9cd3390;

--- a/src/Pure/General/latex.ML	Thu Aug 29 11:43:14 2024 +0200
+++ b/src/Pure/General/latex.ML	Thu Aug 29 17:47:29 2024 +0200
@@ -251,7 +251,9 @@
   else if s = Markup.keyword2N then keyword_markup
   else Markup.no_output;
 
-val _ = Output.add_mode latexN latex_output (prefix Symbol.latex o cartouche);
+fun latex_escape ss = Symbol.latex :: Symbol.open_ :: ss @ [Symbol.close];
+
+val _ = Output.add_mode latexN latex_output latex_escape;
 val _ = Markup.add_mode latexN latex_markup;
 
 val _ = Pretty.add_mode latexN

--- a/src/Pure/General/output.ML	Thu Aug 29 11:43:14 2024 +0200
+++ b/src/Pure/General/output.ML	Thu Aug 29 17:47:29 2024 +0200
@@ -17,11 +17,11 @@
   include BASIC_OUTPUT
   type output = string
   val default_output: string -> output * int
-  val default_escape: output -> string
-  val add_mode: string -> (string -> output * int) -> (output -> string) -> unit
+  val default_escape: output list -> string list
+  val add_mode: string -> (string -> output * int) -> (output list -> string list) -> unit
   val output_width: string -> output * int
   val output: string -> output
-  val escape: output -> string
+  val escape: output list -> string list
   val physical_stdout: output -> unit
   val physical_stderr: output -> unit
   val physical_writeln: output -> unit
@@ -66,7 +66,7 @@
 type output = string;  (*raw system output*)
 
 fun default_output s = (s, size s);
-fun default_escape (s: output) = s;
+fun default_escape (ss: output list) = ss;
 
 local
   val default = {output = default_output, escape = default_escape};

--- a/src/Pure/General/pretty.ML	Thu Aug 29 11:43:14 2024 +0200
+++ b/src/Pure/General/pretty.ML	Thu Aug 29 17:47:29 2024 +0200
@@ -65,11 +65,11 @@
   val regularN: string
   val symbolicN: string
   val output_buffer: int option -> T -> Buffer.T
-  val output: int option -> T -> Output.output
+  val output: int option -> T -> Output.output list
   val string_of_margin: int -> T -> string
   val string_of: T -> string
   val writeln: T -> unit
-  val symbolic_output: T -> Output.output
+  val symbolic_output: T -> Output.output list
   val symbolic_string_of: T -> string
   val unformatted_string_of: T -> string
   val markup_chunks: Markup.T -> T list -> T
@@ -359,15 +359,15 @@
   then symbolic prt
   else formatted (the_default (! margin_default) margin) prt;
 
-val output = Buffer.content oo output_buffer;
-fun string_of_margin margin = Output.escape o output (SOME margin);
-val string_of = Output.escape o output NONE;
-val writeln = Output.writeln o string_of;
+val output = Buffer.contents oo output_buffer;
+fun string_of_margin margin = implode o Output.escape o output (SOME margin);
+val string_of = implode o Output.escape o output NONE;
+val writeln = Output.writelns o Output.escape o output NONE;
 
-val symbolic_output = Buffer.content o symbolic;
-val symbolic_string_of = Output.escape o symbolic_output;
+val symbolic_output = Buffer.contents o symbolic;
+val symbolic_string_of = implode o Output.escape o symbolic_output;
 
-val unformatted_string_of = Output.escape o Buffer.content o unformatted;
+val unformatted_string_of = implode o Output.escape o Buffer.contents o unformatted;
 
 
 (* chunks *)

--- a/src/Pure/PIDE/markup.ML	Thu Aug 29 11:43:14 2024 +0200
+++ b/src/Pure/PIDE/markup.ML	Thu Aug 29 17:47:29 2024 +0200
@@ -864,8 +864,8 @@
 val enclose = output #-> Library.enclose;
 
 fun markup m =
-  let val (bg, en) = output m
-  in Library.enclose (Output.escape bg) (Output.escape en) end;
+  let val (bg, en) = output m |> apply2 (single #> Output.escape #> implode);
+  in Library.enclose bg en end;
 
 val markups = fold_rev markup;
 

--- a/src/Pure/Syntax/syntax_phases.ML	Thu Aug 29 11:43:14 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Aug 29 17:47:29 2024 +0200
@@ -766,7 +766,7 @@
       if show_markup andalso not show_types then
         let
           val ((bg1, bg2), en) = typing_elem;
-          val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty ty) ^ bg2;
+          val bg = implode (bg1 :: Pretty.symbolic_output (pretty_typ_ast Markup.empty 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 = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty s) ^ bg2;
+          val bg = implode (bg1 :: Pretty.symbolic_output (pretty_typ_ast Markup.empty 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