clarified persistent datatype: more direct literal_markup, which also serves as a flag;

--- a/src/Pure/Syntax/lexicon.ML	Wed Sep 25 10:48:16 2024 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Wed Sep 25 12:59:43 2024 +0200
@@ -40,8 +40,6 @@
   val terminals: string list
   val is_terminal: string -> bool
   val get_terminal: string -> token option
-  val suppress_literal_markup: string -> bool
-  val suppress_markup: token -> bool
   val literal_markup: string -> Markup.T list
   val reports_of_token: token -> Position.report list
   val reported_token_range: Proof.context -> token -> string
@@ -199,9 +197,6 @@
 
 (* markup *)
 
-val suppress_literal_markup = Symbol.has_control_block o Symbol.explode;
-fun suppress_markup tok = is_literal tok andalso suppress_literal_markup (str_of_token tok);
-
 fun literal_markup s =
   let val syms = Symbol.explode s in
     if Symbol.has_control_block syms then []

--- a/src/Pure/Syntax/printer.ML	Wed Sep 25 10:48:16 2024 +0200
+++ b/src/Pure/Syntax/printer.ML	Wed Sep 25 12:59:43 2024 +0200
@@ -68,7 +68,7 @@
 datatype symb =
   Arg of int |
   TypArg of int |
-  String of bool * string |
+  String of Markup.T list * string |
   Break of int |
   Block of Syntax_Ext.block * symb list;
 
@@ -139,12 +139,11 @@
           (if Lexicon.is_terminal s then 1000 else p);
 
         fun make_symbs (Syntax_Ext.Delim s :: xsyms) =
-              apfst (cons (String (not (Lexicon.suppress_literal_markup s), s)))
-                (make_symbs xsyms)
+              apfst (cons (String (Lexicon.literal_markup s, s))) (make_symbs xsyms)
           | make_symbs (Syntax_Ext.Argument s_p :: xsyms) =
               apfst (cons (arg s_p)) (make_symbs xsyms)
           | make_symbs (Syntax_Ext.Space s :: xsyms) =
-              apfst (cons (String (false, s))) (make_symbs xsyms)
+              apfst (cons (String ([], s))) (make_symbs xsyms)
           | make_symbs (Syntax_Ext.Bg block :: xsyms) =
               let
                 val (bsyms, xsyms') = make_symbs xsyms;
@@ -234,13 +233,10 @@
                 |> Config.put pretty_priority p
               in (pretty ctxt' tabs trf markup_trans markup_extern t @ Ts, args') end
           end
-      | synT m (String (do_mark, s) :: symbs, args) =
+      | synT m (String (literal_markup, s) :: symbs, args) =
           let
             val (Ts, args') = synT m (symbs, args);
-            val T =
-              if do_mark
-              then Pretty.marks_str (m @ Lexicon.literal_markup s, s)
-              else Pretty.str s;
+            val T = Pretty.marks_str (if null literal_markup then [] else m @ literal_markup, s);
           in (T :: Ts, args') end
       | synT m (Block ({markup, consistent, unbreakable, indent}, bsymbs) :: symbs, args) =
           let
@@ -258,7 +254,7 @@
 
     and parT m (pr, args, p, p': int) = #1 (synT m
           (if p > p' orelse (show_brackets andalso p' <> 1000 andalso not (is_chain pr)) then
-            [Block (Syntax_Ext.block_indent 1, String (false, "(") :: pr @ [String (false, ")")])]
+            [Block (Syntax_Ext.block_indent 1, String ([], "(") :: pr @ [String ([], ")")])]
            else pr, args))
 
     and atomT a = Pretty.marks_str (#1 markup_extern a, #2 markup_extern a)

--- a/src/Pure/Syntax/syntax_phases.ML	Wed Sep 25 10:48:16 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Sep 25 12:59:43 2024 +0200
@@ -158,8 +158,8 @@
     val append_reports = Position.append_reports reports;
 
     fun report_pos tok =
-      if Lexicon.suppress_markup tok then Position.none
-      else Lexicon.pos_of_token tok;
+      if Lexicon.is_literal tok andalso null (Lexicon.literal_markup (Lexicon.str_of_token tok))
+      then Position.none else Lexicon.pos_of_token tok;
 
     fun trans a args =
       (case trf a of