# 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;