--- a/src/Pure/General/pretty.ML Sat Dec 28 23:44:56 2024 +0100
+++ b/src/Pure/General/pretty.ML Sun Dec 29 00:00:41 2024 +0100
@@ -387,6 +387,7 @@
val indent_markup = #indent_markup ops;
val no_indent_markup = indent_markup = Markup.no_output;
+ val (indent_bg, indent_en) = apply2 Substring.full indent_markup;
val add_indent = if no_indent_markup then K I else output_spaces_buffer ops;
@@ -396,7 +397,7 @@
val indent =
if no_indent_markup then Bytes.add (Symbol.spaces n)
else if s = "" then I
- else Bytes.add (#1 indent_markup) #> Bytes.add s #> Bytes.add (#2 indent_markup);
+ else Bytes.add_substring indent_bg #> Bytes.add s #> Bytes.add_substring indent_en;
val tx' = tx |> Bytes.add newline |> indent;
val ind' = Buffer.add s Buffer.empty;
in {tx = tx', ind = ind', pos = n, nl = nl + 1} end;