# HG changeset patch
# User wenzelm
# Date 1724441529 -7200
# Node ID c7f7e58509af9f616dccfe1fb10b1a98afae7644
# Parent  1319c729c65df6a59c6e00409354802f06a82705
more accurate markup (amending 43c4817375bf): only consider primitive syntax consts, avoid extra Markup.intensify e.g. due to "\<^const>Pure.all_binder";

diff -r 1319c729c65d -r c7f7e58509af src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Aug 23 20:45:54 2024 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Aug 23 21:32:09 2024 +0200
@@ -475,7 +475,10 @@
     "Cycle in syntax consts: " ^ (space_implode " \<leadsto> " (map quote cs))) css));
 
 fun get_consts (Syntax ({consts, ...}, _)) c =
-  if Graph.defined consts c then Graph.all_preds consts [c] else [c];
+  if Graph.defined consts c then
+    Graph.all_preds consts [c]
+    |> filter (Graph.Keys.is_empty o Graph.imm_preds consts)
+  else [c];
 
 fun update_consts (c, bs) consts =
   if c = "" orelse (null bs andalso (Lexicon.is_marked c orelse Graph.defined consts c))