more detailed parse tree: retain nonterminal context as well;

--- a/src/Pure/Syntax/parser.ML	Sun Sep 29 15:08:38 2024 +0200
+++ b/src/Pure/Syntax/parser.ML	Sun Sep 29 15:24:17 2024 +0200
@@ -13,7 +13,7 @@
   val pretty_gram: gram -> Pretty.T list
   datatype tree =
     Markup of Markup.T list * tree list |
-    Node of string * tree list |
+    Node of {nonterm: string, const: string} * tree list |
     Tip of Lexicon.token
   val pretty_tree: tree -> Pretty.T list
   val parse: gram -> string -> Lexicon.token list -> tree list
@@ -513,13 +513,13 @@
 
 datatype tree =
   Markup of Markup.T list * tree list |
-  Node of string * tree list |
+  Node of {nonterm: string, const: string} * tree list |
   Tip of Lexicon.token;
 
 datatype tree_op =
   Markup_Push |
   Markup_Pop of Markup.T list |
-  Node_Op of string * tree_op list |
+  Node_Op of {nonterm: int, const: string} * tree_op list |
   Tip_Op of Lexicon.token;
 
 local
@@ -531,7 +531,7 @@
     if pointer_eq arg then EQUAL
     else
       (case apply2 drop_markup arg of
-        (Node_Op (s, ts) :: rest, Node_Op (s', ts') :: rest') =>
+        (Node_Op ({const = s, ...}, ts) :: rest, Node_Op ({const = s', ...}, ts') :: rest') =>
           (case fast_string_ord (s, s') of
             EQUAL =>
               (case tree_ops_ord (ts, ts') of
@@ -550,7 +550,7 @@
       | _ => raise Match);
 end;
 
-fun make_tree tree_ops =
+fun make_tree names tree_ops =
   let
     fun top [] = []
       | top (xs :: _) = xs;
@@ -558,17 +558,20 @@
     fun pop [] = []
       | pop (_ :: xs) = xs;
 
+    fun make_name {nonterm = nt, const} =
+      {nonterm = the_name names nt, const = const};
+
     fun make body stack ops =
       (case ops of
         Markup_Push :: rest => make [] (body :: stack) rest
       | Markup_Pop markup :: rest => make (Markup (markup, body) :: top stack) (pop stack) rest
-      | Node_Op (id, ts) :: rest => make (Node (id, make [] [] ts) :: body) stack rest
+      | Node_Op (name, ts) :: rest => make (Node (make_name name, make [] [] ts) :: body) stack rest
       | Tip_Op tok :: rest => make (Tip tok :: body) stack rest
       | [] => if null stack then body else raise Fail "Pending markup blocks");
  in (case make [] [] tree_ops of [t] => SOME t | _ => NONE) end;
 
 fun pretty_tree (Markup (_, ts)) = maps pretty_tree ts
-  | pretty_tree (Node (c, ts)) =
+  | pretty_tree (Node ({const = c, ...}, ts)) =
       [Pretty.enclose "(" ")" (Pretty.breaks (Pretty.quote (Pretty.str c) :: maps pretty_tree ts))]
   | pretty_tree (Tip tok) =
       if Lexicon.valued_token tok then [Pretty.str (Lexicon.str_of_token tok)] else [];
@@ -593,7 +596,7 @@
 val output_ord = pointer_eq_ord (fn (Output (m, ss), Output (n, tt)) =>
   (case int_ord (m, n) of EQUAL => tree_ops_ord (ss, tt) | ord => ord));
 
-fun output_tree (Output (_, ts)) = make_tree ts;
+fun output_tree names (Output (_, ts)) = make_tree names ts;
 
 end;
 
@@ -693,7 +696,7 @@
           | [] => (*completer operation*)
               let
                 val (A, p, id, j) = info;
-                val out' = if id = "" then out else node_output id out;
+                val out' = node_output {nonterm = A, const = id} out;
                 val (used', Slist) =
                   if j = i then (*lambda production?*)
                     let val (q, used') = update_output (A, (out', p)) used
@@ -732,7 +735,7 @@
 
 in
 
-fun parse (gram as Gram {tags, ...}) start toks =
+fun parse (gram as Gram {tags, names, ...}) start toks =
   let
     val start_tag =
       (case tags_lookup tags start of
@@ -752,7 +755,7 @@
 
     val result =
       produce gram stateset 0 Lexicon.dummy input
-      |> map_filter (output_tree o #3);
+      |> map_filter (output_tree names o #3);
   in if null result then raise Fail "Inner syntax: no parse trees" else result end;
 
 end;

--- a/src/Pure/Syntax/syntax_phases.ML	Sun Sep 29 15:08:38 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Sun Sep 29 15:24:17 2024 +0200
@@ -186,13 +186,14 @@
       [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
-      | asts_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
+      | asts_of (Parser.Node ({const = "", ...}, pts)) = maps asts_of pts
+      | asts_of (Parser.Node ({const = "_class_name", ...}, [Parser.Tip tok])) =
           let
             val pos = report_pos tok;
             val (c, rs) = Proof_Context.check_class ctxt (Lexicon.str_of_token tok, pos);
             val _ = append_reports rs;
           in [Ast.Constant (Lexicon.mark_class c)] end
-      | asts_of (Parser.Node ("_type_name", [Parser.Tip tok])) =
+      | asts_of (Parser.Node ({const = "_type_name", ...}, [Parser.Tip tok])) =
           let
             val pos = report_pos tok;
             val (c, rs) =
@@ -201,15 +202,17 @@
               |>> dest_Type_name;
             val _ = append_reports rs;
           in [Ast.Constant (Lexicon.mark_type c)] end
-      | asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok
-      | asts_of (Parser.Node ("_position_sort", [Parser.Tip tok])) = asts_of_position "_ofsort" tok
-      | asts_of (Parser.Node (a as "\<^const>Pure.dummy_pattern", [Parser.Tip tok])) =
+      | asts_of (Parser.Node ({const = "_position", ...}, [Parser.Tip tok])) =
+          asts_of_position "_constrain" tok
+      | asts_of (Parser.Node ({const = "_position_sort", ...}, [Parser.Tip tok])) =
+          asts_of_position "_ofsort" tok
+      | asts_of (Parser.Node ({const = a as "\<^const>Pure.dummy_pattern", ...}, [Parser.Tip tok])) =
           [ast_of_dummy a tok]
-      | asts_of (Parser.Node (a as "_idtdummy", [Parser.Tip tok])) =
+      | asts_of (Parser.Node ({const = a as "_idtdummy", ...}, [Parser.Tip tok])) =
           [ast_of_dummy a tok]
-      | asts_of (Parser.Node ("_idtypdummy", pts as [Parser.Tip tok, _, _])) =
+      | asts_of (Parser.Node ({const = "_idtypdummy", ...}, pts as [Parser.Tip tok, _, _])) =
           [Ast.Appl (Ast.Constant "_constrain" :: ast_of_dummy "_idtdummy" tok :: maps asts_of pts)]
-      | asts_of (Parser.Node (a, pts)) =
+      | asts_of (Parser.Node ({const = a, ...}, pts)) =
           let val _ = List.app (report_token a) pts;
           in [trans a (maps asts_of pts)] end
       | asts_of (Parser.Tip tok) = asts_of_token tok