# HG changeset patch
# User wenzelm
# Date 1752582330 -7200
# Node ID d19f589fe9ad46bc27ace846044a69d1df99d9e9
# Parent  71e235a7a1ec458fed93b2547381aa0507f43afb
more robust, for typical error message prefix/suffix;

diff -r 71e235a7a1ec -r d19f589fe9ad src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Tue Jul 15 14:24:21 2025 +0200
+++ b/src/Pure/General/pretty.ML	Tue Jul 15 14:25:30 2025 +0200
@@ -243,7 +243,7 @@
   let
     val bs = out prt;
     val bs' =
-      if Bytes.size bs <= String.maxSize then bs
+      if Bytes.size bs + 8000 <= String.maxSize then bs
       else out (from_ML (ML_Pretty.no_markup (to_ML prt)));
   in Bytes.content bs' end;