src/Pure/Syntax/syntax_phases.ML
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