more concrete syntax and more checks;

--- a/src/Pure/Isar/isar_cmd.ML	Fri Aug 23 20:21:04 2024 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Aug 23 20:45:54 2024 +0200
@@ -1,5 +1,5 @@
 (*  Title:      Pure/Isar/isar_cmd.ML
-    Author:     Markus Wenzel, TU Muenchen
+    Author:     Makarius
 
 Miscellaneous Isar commands.
 *)
@@ -15,6 +15,8 @@
   val print_ast_translation: Input.source -> theory -> theory
   val translations: (xstring * string) Syntax.trrule list -> theory -> theory
   val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
+  val syntax_consts: ((string * Position.T) * (xstring * Position.T) list) list -> theory -> theory
+  val syntax_types: ((string * Position.T) * (xstring * Position.T) list) list -> theory -> theory
   val oracle: bstring * Position.range -> Input.source -> theory -> theory
   val declaration: {syntax: bool, pervasive: bool} -> Input.source -> local_theory -> local_theory
   val qed: Method.text_range option -> Toplevel.transition -> Toplevel.transition
@@ -108,6 +110,37 @@
 fun no_translations args thy = Sign.del_trrules (read_trrules thy args) thy;
 
 
+(* syntax consts/types (after translation) *)
+
+local
+
+fun syntax_deps_cmd f args thy =
+  let
+    val ctxt = Proof_Context.init_global thy;
+    fun check_rhs (b: xstring, pos: Position.T) =
+      let
+        val (c, reports) = f ctxt (b, pos);
+        val _ = Context_Position.reports ctxt reports;
+      in c end;
+    fun check_arg (a, bs) = (Proof_Context.check_syntax_const ctxt a, map check_rhs bs);
+  in Sign.syntax_deps (map check_arg args) thy end;
+
+fun check_const ctxt (s, pos) =
+  Proof_Context.check_const {proper = false, strict = true} ctxt (s, [pos])
+  |>> (Term.dest_Const_name #> Lexicon.mark_const);
+
+fun check_type_name ctxt arg =
+  Proof_Context.check_type_name {proper = false, strict = true} ctxt arg
+  |>> (Term.dest_Type_name #> Lexicon.mark_type);
+
+in
+
+val syntax_consts = syntax_deps_cmd check_const;
+val syntax_types = syntax_deps_cmd check_type_name;
+
+end;
+
+
 (* oracles *)
 
 fun oracle (name, range) source =

--- a/src/Pure/Pure.thy	Fri Aug 23 20:21:04 2024 +0200
+++ b/src/Pure/Pure.thy	Fri Aug 23 20:45:54 2024 +0200
@@ -15,9 +15,10 @@
   and "text" "txt" :: document_body
   and "text_raw" :: document_raw
   and "default_sort" :: thy_decl
-  and "typedecl" "nonterminal" "judgment" "consts" "syntax" "no_syntax" "translations"
-    "no_translations" "type_notation" "no_type_notation" "notation" "no_notation" "alias"
-    "type_alias" "declare" "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
+  and "typedecl" "nonterminal" "judgment" "consts" "syntax" "no_syntax" "syntax_consts"
+    "syntax_types" "translations" "no_translations" "type_notation" "no_type_notation" "notation"
+    "no_notation" "alias" "type_alias" "declare" "hide_class" "hide_type" "hide_const"
+    "hide_fact" :: thy_decl
   and "type_synonym" "definition" "abbreviation" "lemmas" :: thy_defn
   and "axiomatization" :: thy_stmt
   and "external_file" "bibtex_file" "ROOTS_file" :: thy_load
@@ -401,6 +402,19 @@
     (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl
       >> uncurry (Local_Theory.syntax_cmd false));
 
+val syntax_consts =
+  Parse.and_list1
+    ((Parse.name_position --| (\<^keyword>\<open>\<rightleftharpoons>\<close> || \<^keyword>\<open>==\<close>)) --
+      Parse.!!! (Scan.repeat1 Parse.name_position));
+
+val _ =
+  Outer_Syntax.command \<^command_keyword>\<open>syntax_consts\<close> "declare syntax const dependencies"
+    (syntax_consts >> (Toplevel.theory o Isar_Cmd.syntax_consts));
+
+val _ =
+  Outer_Syntax.command \<^command_keyword>\<open>syntax_types\<close> "declare syntax const dependencies (type names)"
+    (syntax_consts >> (Toplevel.theory o Isar_Cmd.syntax_types));
+
 val trans_pat =
   Scan.optional
     (\<^keyword>\<open>(\<close> |-- Parse.!!! (Parse.inner_syntax Parse.name --| \<^keyword>\<open>)\<close>)) "logic"