--- a/src/Pure/Syntax/printer.ML Tue Jan 19 14:14:23 2021 +0100
+++ b/src/Pure/Syntax/printer.ML Tue Jan 19 20:23:13 2021 +0100
@@ -138,7 +138,7 @@
(if Lexicon.is_terminal s then 1000 else p);
fun xsyms_to_syms (Syntax_Ext.Delim s :: xsyms) =
- apfst (cons (String (not (exists Symbol.is_block_ctrl (Symbol.explode s)), s)))
+ apfst (cons (String (not (Lexicon.suppress_literal_markup s), s)))
(xsyms_to_syms xsyms)
| xsyms_to_syms (Syntax_Ext.Argument s_p :: xsyms) =
apfst (cons (arg s_p)) (xsyms_to_syms xsyms)
@@ -232,7 +232,7 @@
val (Ts, args') = synT m (symbs, args);
val T =
if do_mark
- then Pretty.marks_str (m @ [Lexicon.literal_markup s], s)
+ then Pretty.marks_str (m @ Lexicon.literal_markup s, s)
else Pretty.str s;
in (T :: Ts, args') end
| synT m (Block ({markup, consistent, unbreakable, indent}, bsymbs) :: symbs, args) =