# HG changeset patch
# User wenzelm
# Date 1734552415 -3600
# Node ID 2d4838ffb67e2e1350e05acfe4b31a709587c4c2
# Parent  5b87f8dacd8e9854a92b5ac219fc282d913656d8
more markup: for diagnostic purposes of ambig_msgs;

diff -r 5b87f8dacd8e -r 2d4838ffb67e src/Pure/PIDE/markup_kind.ML
--- a/src/Pure/PIDE/markup_kind.ML	Wed Dec 18 16:03:07 2024 +0100
+++ b/src/Pure/PIDE/markup_kind.ML	Wed Dec 18 21:06:55 2024 +0100
@@ -17,6 +17,7 @@
   val check_expression: Proof.context -> xstring * Position.T -> Markup.T
   val setup_expression: binding -> Markup.T
   val markup_item: Markup.T
+  val markup_syntax: Markup.T
   val markup_mixfix: Markup.T
   val markup_prefix: Markup.T
   val markup_postfix: Markup.T
@@ -99,6 +100,8 @@
 
 val markup_item = setup_expression (Binding.make ("item", \<^here>));
 
+val markup_syntax = setup_expression (Binding.make ("syntax", \<^here>));
+
 val markup_mixfix = setup_notation (Binding.make ("mixfix", \<^here>));
 val markup_prefix = setup_notation (Binding.make ("prefix", \<^here>));
 val markup_postfix = setup_notation (Binding.make ("postfix", \<^here>));
diff -r 5b87f8dacd8e -r 2d4838ffb67e src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Wed Dec 18 16:03:07 2024 +0100
+++ b/src/Pure/Syntax/parser.ML	Wed Dec 18 21:06:55 2024 +0100
@@ -543,11 +543,15 @@
   end;
 
 fun pretty_tree (Markup (_, ts)) = maps pretty_tree ts
-  | pretty_tree (Node ({const = c, ...}, ts)) =
-      let val body = maps pretty_tree ts in
-        if c = "" then body
-        else [Pretty.enclose "(" ")" (Pretty.breaks (Pretty.quote (Pretty.str c) :: body))]
-      end
+  | pretty_tree (Node ({nonterm = nt, const = c, ...}, ts)) =
+      let
+        fun mark_const body =
+          if c = "" then body
+          else [Pretty.enclose "(" ")" (Pretty.breaks (Pretty.quote (Pretty.str c) :: body))];
+        fun mark_nonterm body =
+          if nt = "" then body
+          else [Pretty.markup_open (Markup.name nt Markup_Kind.markup_syntax) body];
+      in mark_nonterm (mark_const (maps pretty_tree ts))  end
   | pretty_tree (Tip tok) =
       if Lexicon.valued_token tok then [Pretty.str (Lexicon.str_of_token tok)] else [];