# HG changeset patch
# User wenzelm
# Date 1735426841 -3600
# Node ID c48752d477ce6ccc0398f5d120b4aa007c0da42f
# Parent  b31d09029b9459dbcc11775c9faa4d64a7573c74
minor performance tuning;

diff -r b31d09029b94 -r c48752d477ce src/Pure/General/pretty.ML
--- 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;