minor performance tuning;
authorwenzelm
Sun, 29 Dec 2024 00:00:41 +0100
changeset 81684 c48752d477ce
parent 81683 b31d09029b94
child 81685 13bd6223691d
minor performance tuning;
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;