less markup (amending 07ad0b407d38): const = "" is mainly for parentheses syntax -- avoid entity_markup here;
--- a/src/Pure/Syntax/syntax_phases.ML Sun Sep 29 21:16:17 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Sun Sep 29 21:20:36 2024 +0200
@@ -165,7 +165,7 @@
and report_literal a t =
(case t of
Parser.Markup (_, ts) => report_literals a ts
- | Parser.Node ({const, ...}, ts) => if const = "" then report_literals a ts else ()
+ | Parser.Node _ => ()
| Parser.Tip tok =>
if Lexicon.is_literal tok then report (report_pos tok) (markup_entity ctxt) a else ());