# HG changeset patch
# User wenzelm
# Date 1727195136 -7200
# Node ID 501ebf1fc3089508f89088ddc23a34448b4d87de
# Parent  fd7a70babec1ce6153dfbe142a6049ec4fd2d1dc
minor performance tuning for blocks without markup;

diff -r fd7a70babec1 -r 501ebf1fc308 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Tue Sep 24 18:17:39 2024 +0200
+++ b/src/Pure/General/pretty.ML	Tue Sep 24 18:25:36 2024 +0200
@@ -139,10 +139,15 @@
 fun mark m prt = if m = Markup.empty then prt else markup m [prt];
 
 fun markup_blocks ({markup, consistent, indent}: Markup.T list block) body =
-  let
-    val markups = filter_out Markup.is_empty markup;
-    val (ms, m) = if null markups then ([], Markup.empty) else split_last markups;
-  in fold_rev mark ms (markup_block {markup = m, consistent = consistent, indent = indent} body) end;
+  if forall Markup.is_empty markup andalso not consistent then blk (indent, body)
+  else
+    let
+      val markups = filter_out Markup.is_empty markup;
+      val (ms, m) = if null markups then ([], Markup.empty) else split_last markups;
+    in
+      fold_rev mark ms
+        (markup_block {markup = m, consistent = consistent, indent = indent} body)
+    end;
 
 
 (* breaks *)