# HG changeset patch
# User wenzelm
# Date 1727637377 -7200
# Node ID d0cd220d8e8b13d7013bebc2e80f4ba217eecffc
# Parent  719449222c0e1fe915b2dcf284e85ccf0dd54414
more markup reports: notably "notation=..." within pretty blocks;

diff -r 719449222c0e -r d0cd220d8e8b src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sun Sep 29 21:13:17 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Sun Sep 29 21:16:17 2024 +0200
@@ -188,7 +188,8 @@
     fun asts_of_position c tok =
       [Ast.Appl [Ast.Constant c, ast_of (Parser.Tip tok), ast_of_position tok]]
 
-    and asts_of (Parser.Markup (markup, pts)) = maps asts_of pts
+    and asts_of (Parser.Markup ({markup, range = (pos, _), ...}, pts)) =
+          (append_reports (map (pair pos) markup); maps asts_of pts)
       | asts_of (Parser.Node ({const = "", ...}, pts)) = maps asts_of pts
       | asts_of (Parser.Node ({const = "_class_name", ...}, [Parser.Tip tok])) =
           let