more accurate markup (amending 43c4817375bf): only consider primitive syntax consts, avoid extra Markup.intensify e.g. due to "\<^const>Pure.all_binder";

--- 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))