# HG changeset patch
# User wenzelm
# Date 1728897206 -7200
# Node ID 9067932c2182ae6a4b45ab1bdffc3e647c6872ec
# Parent  37c039c308909bf101fd85bdf8266e22b7ed4807
tuned;

diff -r 37c039c30890 -r 9067932c2182 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Mon Oct 14 11:06:03 2024 +0200
+++ b/src/Pure/Syntax/printer.ML	Mon Oct 14 11:13:26 2024 +0200
@@ -283,19 +283,16 @@
       | syntax m (String (literal_markup, s) :: symbs, args) =
           let
             val (prts, args') = syntax m (symbs, args);
-            val prt = Pretty.marks_str (if null literal_markup then [] else m @ literal_markup, s);
-          in (prt :: prts, args') end
+            val m' = if null literal_markup then [] else m @ literal_markup
+          in (Pretty.marks_str (m', s) :: prts, args') end
       | syntax m (Block (block, bsymbs) :: symbs, args) =
           let
             val (body, args') = syntax m (bsymbs, args);
             val (prts, args'') = syntax m (symbs, args');
-            val prt = Syntax_Ext.pretty_block block body;
-          in (prt :: prts, args'') end
+          in (Syntax_Ext.pretty_block block body :: prts, args'') end
       | syntax m (Break i :: symbs, args) =
-          let
-            val (prts, args') = syntax m (symbs, args);
-            val prt = if i < 0 then Pretty.fbrk else Pretty.brk i;
-          in (prt :: prts, args') end;
+          let val (prts, args') = syntax m (symbs, args)
+          in ((if i < 0 then Pretty.fbrk else Pretty.brk i) :: prts, args') end;
 
   in main (Config.get ctxt pretty_priority) end;