clarified order of markup: more uniform input vs. output;
--- 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