# HG changeset patch
# User wenzelm
# Date 1727689372 -7200
# Node ID 8e2114e6205bfb9ece6a4a9ce16660e28d1e60c9
# Parent  ddbfb398d892bdb1bbe3c7010493c560aeaccf95
clarified order of markup: more uniform input vs. output;

diff -r ddbfb398d892 -r 8e2114e6205b src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Mon Sep 30 10:50:33 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Mon Sep 30 11:42:52 2024 +0200
@@ -189,7 +189,10 @@
       [Ast.Appl [Ast.Constant c, ast_of (Parser.Tip tok), ast_of_position tok]]
 
     and asts_of (Parser.Markup ({markup, range = (pos, _), ...}, pts)) =
-          (append_reports (map (pair pos) markup); maps asts_of pts)
+          let
+            val asts = maps asts_of pts;
+            val _ = append_reports (map (pair pos) markup);
+          in asts end
       | asts_of (Parser.Node ({const = "", ...}, pts)) = maps asts_of pts
       | asts_of (Parser.Node ({const = "_class_name", ...}, [Parser.Tip tok])) =
           let