changeset 80952 | a61ed25ba155 |
parent 80950 | b4a6bee4621a |
child 80991 | 2d07d2bbd8c6 |
--- 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