clarified order of markup: more uniform input vs. output;
authorwenzelm
Mon, 30 Sep 2024 11:42:52 +0200
changeset 81016 8e2114e6205b
parent 81015 ddbfb398d892
child 81017 bc5eb7841b74
clarified order of markup: more uniform input vs. output;
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