# HG changeset patch
# User wenzelm
# Date 1745693566 -7200
# Node ID ae1e6ff06b032d199de37b42dfb7a417ed20efbd
# Parent  d08f5b5ead0a294d42ccfe75f05575103c3fd065
more robust output: no markup as last resort;

diff -r d08f5b5ead0a -r ae1e6ff06b03 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Fri Apr 25 18:06:12 2025 +0200
+++ b/src/Pure/General/pretty.ML	Sat Apr 26 20:52:46 2025 +0200
@@ -237,6 +237,17 @@
 
 (** formatting **)
 
+(* robust string output, with potential data loss *)
+
+fun robust_string_of out prt =
+  let
+    val bs = out prt;
+    val bs' =
+      if Bytes.size bs <= String.maxSize then bs
+      else out (from_ML (ML_Pretty.no_markup (to_ML prt)));
+  in Bytes.content bs' end;
+
+
 (* output operations *)
 
 type output_ops =
@@ -501,7 +512,7 @@
       | output (Str (s, _)) = Bytes.add s;
   in Bytes.build o output o output_tree ops false end;
 
-val symbolic_string_of = Bytes.content o symbolic_output;
+val symbolic_string_of = robust_string_of symbolic_output;
 
 
 (* unformatted output: other markup only *)
@@ -516,14 +527,14 @@
   in Bytes.build o output o output_tree ops false end;
 
 fun unformatted_string_of prt =
-  Bytes.content (unformatted (output_ops NONE) prt);
+  robust_string_of (unformatted (output_ops NONE)) prt;
 
 
 (* output interfaces *)
 
 fun output ops = if #symbolic ops then symbolic_output else format_tree ops;
 
-fun string_of_ops ops = Bytes.content o output ops;
+fun string_of_ops ops = robust_string_of (output ops);
 fun string_of prt = string_of_ops (output_ops NONE) prt;
 
 fun strings_of prt = Bytes.contents (output (output_ops NONE) prt);
diff -r d08f5b5ead0a -r ae1e6ff06b03 src/Pure/ML/ml_pretty.ML
--- a/src/Pure/ML/ml_pretty.ML	Fri Apr 25 18:06:12 2025 +0200
+++ b/src/Pure/ML/ml_pretty.ML	Sat Apr 26 20:52:46 2025 +0200
@@ -9,9 +9,11 @@
   datatype context = datatype PolyML.context
   val markup_get: PolyML.context list -> string * string
   val markup_context: string * string -> PolyML.context list
+  val no_markup_context: PolyML.context list -> PolyML.context list
   val open_block_detect: PolyML.context list -> bool
   val open_block_context: bool -> PolyML.context list
   datatype pretty = datatype PolyML.pretty
+  val no_markup: pretty -> pretty
   val block: pretty list -> pretty
   val str: string -> pretty
   val brk: FixedInt.int -> pretty
@@ -58,6 +60,9 @@
   (if bg = "" then [] else [ContextProperty (markup_bg, bg)]) @
   (if en = "" then [] else [ContextProperty (markup_en, en)]);
 
+val no_markup_context =
+  List.filter (fn ContextProperty (a, _) => a <> markup_bg andalso a <> markup_en | _ => true);
+
 
 (* open_block flag *)
 
@@ -77,6 +82,9 @@
 
 datatype pretty = datatype PolyML.pretty;
 
+fun no_markup (PrettyBlock (a, b, c, d)) = PrettyBlock (a, b, no_markup_context c, map no_markup d)
+  | no_markup a = a;
+
 fun block prts = PrettyBlock (2, false, [], prts);
 val str = PrettyString;
 fun brk width = PrettyBreak (width, 0);