# HG changeset patch
# User wenzelm
# Date 1735484327 -3600
# Node ID 84f1951bcc3c8fb3250372988e644607b84fc435
# Parent  442af2d573f9f203780f1cd55ad3db09c1de965d
tuned: more uniform;

diff -r 442af2d573f9 -r 84f1951bcc3c src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Sun Dec 29 15:49:11 2024 +0100
+++ b/src/Pure/General/pretty.ML	Sun Dec 29 15:58:47 2024 +0100
@@ -402,7 +402,7 @@
       | format (prt :: prts, block as (_, blockin), after) (text as {ind, pos, nl, ...}) =
           (case prt of
             Block {markup = (bg, en), open_block = true, body, ...} =>
-              format (Raw bg :: body @ Raw en :: prts, block, after) text
+              text |> raw bg |> format (body @ Raw en :: prts, block, after)
           | Block {markup = (bg, en), consistent, indent, body, length = blen, ...} =>
               let
                 val pos' = pos + indent;
@@ -414,10 +414,8 @@
                 val after' = break_dist (prts, after)
                 val body' = body
                   |> (consistent andalso pos + blen > margin - after') ? map force_break;
-                val btext: text = text
-                  |> raw bg
-                  |> format (body', block', after')
-                  |> raw en;
+                val btext: text =
+                  text |> raw bg |> format (body' @ [Raw en], block', after');
                 (*if this block was broken then force the next break*)
                 val prts' = if nl < #nl btext then force_next prts else prts;
               in format (prts', block, after) btext end