# HG changeset patch
# User wenzelm
# Date 1729591426 -7200
# Node ID 2157039256d3cc8eecc783e39025bd585abb0ba5
# Parent  f63ffe7f4234e5279c4fc574234f4275af25501a
clarified markers for syntax consts: avoid overlap with logical consts;

diff -r f63ffe7f4234 -r 2157039256d3 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Mon Oct 21 22:58:14 2024 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Tue Oct 22 12:03:46 2024 +0200
@@ -60,6 +60,9 @@
   val read_int: string -> int option
   val read_num: string -> {radix: int, leading_zeros: int, value: int}
   val read_float: string -> {mant: int, exp: int}
+  val mark_syntax: string -> string
+  val mark_binder: string -> string
+  val mark_indexed: string -> string
   val mark_class: string -> string val unmark_class: string -> string val is_class: string -> bool
   val mark_type: string -> string val unmark_type: string -> string val is_type: string -> bool
   val mark_const: string -> string val unmark_const: string -> string val is_const: string -> bool
@@ -474,10 +477,21 @@
   end;
 
 
-(* marked logical entities *)
+
+(** marked names **)
 
 fun marker s = (prefix s, unprefix s, String.isPrefix s);
 
+
+(* syntax consts *)
+
+val (mark_syntax, _, _) = marker "\<^syntax>";
+val (mark_binder, _, _) = marker "\<^binder>";
+val (mark_indexed, _, _) = marker "\<^indexed>";
+
+
+(* logical entities *)
+
 val (mark_class, unmark_class, is_class) = marker "\<^class>";
 val (mark_type, unmark_type, is_type) = marker "\<^type>";
 val (mark_const, unmark_const, is_const) = marker "\<^const>";
diff -r f63ffe7f4234 -r 2157039256d3 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Mon Oct 21 22:58:14 2024 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Tue Oct 22 12:03:46 2024 +0200
@@ -30,7 +30,6 @@
   val default_constraint: Proof.context -> mixfix -> typ
   val make_type: int -> typ
   val binder_name: string -> string
-  val is_binder_name: string -> bool
   val syn_ext_types: Proof.context -> (string * typ * mixfix) list -> Syntax_Ext.syn_ext
   val syn_ext_consts: Proof.context -> string list -> (string * typ * mixfix) list ->
     Syntax_Ext.syn_ext
@@ -171,9 +170,7 @@
 (* binder notation *)
 
 val binder_stamp = stamp ();
-val binder_suffix = "_binder"
-val binder_name = suffix binder_suffix;
-val is_binder_name = String.isSuffix binder_suffix;
+val binder_name = perhaps (try Lexicon.unmark_const) #> Lexicon.mark_binder;
 
 val binder_bg = Symbol_Pos.explode0 "(";
 val binder_en = Symbol_Pos.explode0 "_./ _)";
diff -r f63ffe7f4234 -r 2157039256d3 src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Mon Oct 21 22:58:14 2024 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Tue Oct 22 12:03:46 2024 +0200
@@ -383,7 +383,7 @@
       else
         let
           val indexed_const =
-            if const <> "" then const ^ "_indexed"
+            if const <> "" then Lexicon.mark_indexed const
             else err_in_mixfix "Missing constant name for indexed syntax";
           val rangeT = Term.range_type typ handle Match =>
             err_in_mixfix "Missing structure argument for indexed syntax";
diff -r f63ffe7f4234 -r 2157039256d3 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Mon Oct 21 22:58:14 2024 +0200
+++ b/src/Pure/pure_thy.ML	Tue Oct 22 12:03:46 2024 +0200
@@ -219,7 +219,7 @@
     ("_lambda",           typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic",
       mixfix ("(\<open>indent=3 notation=abstraction\<close>%_./ _)", [0, 3], 3)),
     (const "Pure.eq",     typ "'a \<Rightarrow> 'a \<Rightarrow> prop",       infix_ ("==", 2)),
-    (const "Pure.all_binder", typ "idts \<Rightarrow> prop \<Rightarrow> prop",
+    (Mixfix.binder_name "Pure.all", typ "idts \<Rightarrow> prop \<Rightarrow> prop",
       mixfix ("(\<open>indent=3 notation=\<open>binder !!\<close>\<close>!!_./ _)", [0, 0], 0)),
     (const "Pure.imp",    typ "prop \<Rightarrow> prop \<Rightarrow> prop",   infixr_ ("==>", 1)),
     ("_DDDOT",            typ "aprop",                  Mixfix.mixfix "..."),