# HG changeset patch
# User wenzelm
# Date 1727192124 -7200
# Node ID a119154a5f27a2d2cd2293a25f828bd66ddbc966
# Parent  bdb63d71bf07df355466b834043a463a00edfcdb
minor performance tuning: more direct blocks without markup;
tuned signature;

diff -r bdb63d71bf07 -r a119154a5f27 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Tue Sep 24 17:31:12 2024 +0200
+++ b/src/Pure/General/pretty.ML	Tue Sep 24 17:35:24 2024 +0200
@@ -27,16 +27,16 @@
   type T
   val to_ML: T -> ML_Pretty.pretty
   val from_ML: ML_Pretty.pretty -> T
-  type 'a block = {markup: 'a, consistent: bool, indent: int}
-  val make_block: Markup.output block -> T list -> T
-  val markup_block: Markup.T block -> T list -> T
-  val markup_blocks: Markup.T list block -> T list -> T
-  val markup: Markup.T -> T list -> T
-  val mark: Markup.T -> T -> T
   val blk: int * T list -> T
   val block0: T list -> T
   val block1: T list -> T
   val block: T list -> T
+  type 'a block = {markup: 'a, consistent: bool, indent: int}
+  val make_block: Markup.output block -> T list -> T
+  val markup_block: Markup.T block -> T list -> T
+  val markup: Markup.T -> T list -> T
+  val mark: Markup.T -> T -> T
+  val markup_blocks: Markup.T list block -> T list -> T
   val str: string -> T
   val dots: T
   val brk: int -> T
@@ -115,6 +115,16 @@
 
 (* blocks *)
 
+fun blk (indent, body) =
+  from_ML (ML_Pretty.PrettyBlock (short_nat indent, false, [], map to_ML body));
+
+fun block0 body = blk (0, body);
+fun block1 body = blk (1, body);
+fun block body = blk (2, body);
+
+
+(* blocks with markup *)
+
 type 'a block = {markup: 'a, consistent: bool, indent: int}
 
 fun make_block ({markup, consistent, indent}: Markup.output block) body =
@@ -134,13 +144,6 @@
     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;
 
-fun blk (indent, body) =
-  markup_block {markup = Markup.empty, consistent = false, indent = indent} body;
-
-fun block0 body = blk (0, body);
-fun block1 body = blk (1, body);
-fun block body = blk (2, body);
-
 
 (* breaks *)