tuned;
authorwenzelm
Mon, 14 Oct 2024 11:13:26 +0200
changeset 81162 9067932c2182
parent 81161 37c039c30890
child 81163 2301ec62fdca
tuned;
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;