# HG changeset patch
# User wenzelm
# Date 1724612060 -7200
# Node ID 079fe4292526a2d458f06dfd93ba94a922354e3a
# Parent  72beac575e9c1ab61ea49ad328e92cef5a84f16c
clarified Syntax.is_const (after 43c4817375bf): exclude logical consts from 'syntax_consts' / 'syntax_types', e.g. relevant for @{syntax_const} antiquotation;

diff -r 72beac575e9c -r 079fe4292526 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sun Aug 25 16:00:59 2024 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sun Aug 25 20:54:20 2024 +0200
@@ -442,7 +442,9 @@
       | NONE => Printer.get_binder prtabs c)
       |> Option.map Prefix);
 
-fun is_const (Syntax ({consts, ...}, _)) = Graph.defined consts;
+fun is_const (Syntax ({consts, ...}, _)) c =
+  Graph.defined consts c andalso not (Lexicon.is_marked c);
+
 fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;
 fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon;
 fun parse (Syntax ({gram, ...}, _)) = Parser.parse (cache_eval gram);