# HG changeset patch
# User wenzelm
# Date 1735425896 -3600
# Node ID b31d09029b9459dbcc11775c9faa4d64a7573c74
# Parent  2f98e3c4592c70ca21dbac1e72d2d17d1bf22f02
clarified signature: more direct indent_markup;
minor performance tuning: bypass "ind" buffer when unused;

diff -r 2f98e3c4592c -r b31d09029b94 src/Pure/General/latex.ML
--- a/src/Pure/General/latex.ML	Sat Dec 28 15:43:30 2024 +0100
+++ b/src/Pure/General/latex.ML	Sat Dec 28 23:44:56 2024 +0100
@@ -244,7 +244,7 @@
 local
 
 val markup_macro = YXML.output_markup o Markup.latex_macro;
-val markup_indent = markup_macro "isaindent";
+
 val markup_latex =
  Symtab.make
   [(Markup.commandN, markup_macro "isakeywordONE"),
@@ -272,16 +272,13 @@
     SOME (XML.Elem (m, _)) => latex_markup m
   | _ => Markup.no_output);
 
-fun latex_indent s (_: int) =
-  if s = "" then s else uncurry enclose markup_indent s;
-
 in
 
 fun output_ops opt_margin : Pretty.output_ops =
  {symbolic = false,
   output = output_width,
   markup = latex_markup_output,
-  indent = latex_indent,
+  indent_markup = markup_macro "isaindent",
   margin = ML_Pretty.get_margin opt_margin};
 
 end;
diff -r 2f98e3c4592c -r b31d09029b94 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Sat Dec 28 15:43:30 2024 +0100
+++ b/src/Pure/General/pretty.ML	Sat Dec 28 23:44:56 2024 +0100
@@ -75,7 +75,7 @@
    {symbolic: bool,
     output: string -> Output.output * int,
     markup: Markup.output -> Markup.output,
-    indent: string -> int -> Output.output,
+    indent_markup: Markup.output,
     margin: int}
   val output_ops: int option -> output_ops
   val pure_output_ops: int option -> output_ops
@@ -243,14 +243,14 @@
  {symbolic: bool,
   output: string -> Output.output * int,
   markup: Markup.output -> Markup.output,
-  indent: string -> int -> Output.output,
+  indent_markup: Markup.output,
   margin: int};
 
 fun make_output_ops {symbolic, markup} opt_margin : output_ops =
  {symbolic = symbolic,
   output = fn s => (s, size s),
   markup = markup,
-  indent = fn _ => Symbol.spaces,
+  indent_markup = Markup.no_output,
   margin = ML_Pretty.get_margin opt_margin};
 
 val pure_output_ops = make_output_ops {symbolic = false, markup = K Markup.no_output};
@@ -382,17 +382,24 @@
     val breakgain = margin div 20;     (*minimum added space required of a break*)
     val emergencypos = margin div 2;   (*position too far to right*)
 
-    val linebreak = newline (output_newline ops);
+    val newline = output_newline ops;
     val blanks = string o output_spaces ops;
-    val blanks_buffer = output_spaces_buffer ops;
+
+    val indent_markup = #indent_markup ops;
+    val no_indent_markup = indent_markup = Markup.no_output;
+
+    val add_indent = if no_indent_markup then K I else output_spaces_buffer ops;
 
-    fun indentation (buf, len) {tx, ind, pos, nl} : text =
-      let val s = Buffer.content buf in
-       {tx = Bytes.add (#indent ops s len) tx,
-        ind = Buffer.add s ind,
-        pos = pos + len,
-        nl = nl}
-      end;
+    fun break_indent (buf, n) ({tx, nl, ...}: text) : text =
+      let
+        val s = Buffer.content buf;
+        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);
+        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;
 
     (*blockin is the indentation of the current block;
       after is the width of the following context until next break.*)
@@ -406,8 +413,9 @@
                 val pos' = pos + indent;
                 val pos'' = pos' mod emergencypos;
                 val block' =
-                  if pos' < emergencypos then (ind |> blanks_buffer indent, pos')
-                  else (blanks_buffer pos'' Buffer.empty, pos'');
+                  if pos' < emergencypos
+                  then (add_indent indent ind, pos')
+                  else (add_indent pos'' Buffer.empty, pos'');
                 val d = break_dist (prts, after)
                 val body' = body |> (consistent andalso pos + blen > margin - d) ? map force_break;
                 val btext: text = text
@@ -424,7 +432,7 @@
                 (if not force andalso
                     pos + wd <= Int.max (margin - break_dist (prts, after), blockin + breakgain)
                  then text |> blanks wd  (*just insert wd blanks*)
-                 else text |> linebreak |> indentation block |> blanks ind)
+                 else text |> break_indent block |> blanks ind)
           | Str str => format (prts, block, after) (string str text)
           | Raw s => format (prts, block, after) (raw s text));
   in