minor performance tuning for blocks without markup;
authorwenzelm
Tue, 24 Sep 2024 18:25:36 +0200
changeset 80942 501ebf1fc308
parent 80941 fd7a70babec1
child 80943 258b76a8b099
minor performance tuning for blocks without markup;
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 *)