commands 'syntax_types' and 'syntax_consts' now work in a local theory context;

--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Sat Dec 14 22:26:27 2024 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Sat Dec 14 23:48:45 2024 +0100
@@ -1121,8 +1121,8 @@
     @{command_def "nonterminal"} & : & \<open>theory \<rightarrow> theory\<close> \\
     @{command_def "syntax"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
     @{command_def "no_syntax"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
-    @{command_def "syntax_types"} & : & \<open>theory \<rightarrow> theory\<close> \\
-    @{command_def "syntax_consts"} & : & \<open>theory \<rightarrow> theory\<close> \\
+    @{command_def "syntax_types"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
+    @{command_def "syntax_consts"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
     @{command_def "translations"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
     @{command_def "no_translations"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
     @{attribute_def syntax_ast_trace} & : & \<open>attribute\<close> & default \<open>false\<close> \\

--- a/src/Pure/Isar/isar_cmd.ML	Sat Dec 14 22:26:27 2024 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Dec 14 23:48:45 2024 +0100
@@ -15,9 +15,9 @@
   val print_ast_translation: Input.source -> theory -> theory
   val translations: bool -> (string * string) Syntax.trrule list -> theory -> theory
   val syntax_consts: ((string * Position.T) list * (xstring * Position.T) list) list ->
-    theory -> theory
+    local_theory -> local_theory
   val syntax_types: ((string * Position.T) list * (xstring * Position.T) list) list ->
-    theory -> theory
+    local_theory -> local_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,15 +108,13 @@
 
 local
 
-fun syntax_deps_cmd f args thy =
+fun syntax_deps_cmd f args lthy =
   let
-    val ctxt = Proof_Context.init_global thy;
-
-    val check_lhs = Proof_Context.check_syntax_const ctxt;
+    val check_lhs = Proof_Context.check_syntax_const lthy;
     fun check_rhs (b: xstring, pos: Position.T) =
       let
-        val (c: string, reports) = f ctxt (b, pos);
-        val _ = Context_Position.reports ctxt reports;
+        val (c: string, reports) = f lthy (b, pos);
+        val _ = Context_Position.reports lthy reports;
       in c end;
 
     fun check (raw_lhs, raw_rhs) =
@@ -124,15 +122,15 @@
         val lhs = map check_lhs raw_lhs;
         val rhs = map check_rhs raw_rhs;
       in map (fn l => (l, rhs)) lhs end;
-  in Sign.syntax_deps (maps check args) thy end;
+  in Local_Theory.syntax_deps (maps check args) lthy end;
 
 fun check_const ctxt (s, pos) =
   Proof_Context.check_const {proper = true, strict = false} ctxt (s, [pos])
-  |>> (Term.dest_Const_name #> Lexicon.mark_const);
+  |>> (Term.dest_Const_name #> Lexicon.mark_const #> tap (Sign.check_syntax_dep ctxt));
 
 fun check_type_name ctxt arg =
   Proof_Context.check_type_name {proper = true, strict = false} ctxt arg
-  |>> (Term.dest_Type_name #> Lexicon.mark_type);
+  |>> (Term.dest_Type_name #> Lexicon.mark_type #> tap (Sign.check_syntax_dep ctxt));
 
 in
 

--- a/src/Pure/Isar/local_theory.ML	Sat Dec 14 22:26:27 2024 +0100
+++ b/src/Pure/Isar/local_theory.ML	Sat Dec 14 23:48:45 2024 +0100
@@ -67,6 +67,7 @@
     local_theory -> local_theory
   val syntax_cmd: bool -> Syntax.mode -> (string * string * mixfix) list ->
     local_theory -> local_theory
+  val syntax_deps: (string * string list) list -> Proof.context -> local_theory
   val translations: bool -> Ast.ast Syntax.trrule list -> local_theory -> local_theory
   val translations_cmd: bool -> (string * string) Syntax.trrule list -> local_theory -> local_theory
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
@@ -335,6 +336,10 @@
 val syntax = gen_syntax (K I);
 val syntax_cmd = gen_syntax Proof_Context.read_typ_syntax;
 
+fun syntax_deps args =
+  declaration {syntax = true, pervasive = false, pos = Position.thread_data ()}
+    (fn _ => Proof_Context.generic_syntax_deps args);
+
 
 (* translations *)
 

--- a/src/Pure/Isar/proof_context.ML	Sat Dec 14 22:26:27 2024 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sat Dec 14 23:48:45 2024 +0100
@@ -167,6 +167,7 @@
     Proof.context -> Proof.context
   val generic_syntax: bool -> Syntax.mode -> (string * typ * mixfix) list ->
     Context.generic -> Context.generic
+  val generic_syntax_deps: (string * string list) list -> Context.generic -> Context.generic
   val translations: bool -> Ast.ast Syntax.trrule list -> Proof.context -> Proof.context
   val generic_translations: bool -> Ast.ast Syntax.trrule list -> Context.generic -> Context.generic
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> Proof.context -> Proof.context
@@ -1219,6 +1220,10 @@
 fun generic_syntax add mode args =
   Context.mapping (Sign.syntax_global add mode args) (syntax add mode args);
 
+fun generic_syntax_deps args =
+  Context.mapping (Sign.syntax_deps args)
+    (fn ctxt => map_syntax (Local_Syntax.syntax_deps ctxt args) ctxt);
+
 
 (* translations *)
 

--- a/src/Pure/Pure.thy	Sat Dec 14 22:26:27 2024 +0100
+++ b/src/Pure/Pure.thy	Sat Dec 14 23:48:45 2024 +0100
@@ -408,12 +408,12 @@
       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));
+  Outer_Syntax.local_theory \<^command_keyword>\<open>syntax_consts\<close> "declare syntax const dependencies"
+    (syntax_consts >> 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));
+  Outer_Syntax.local_theory \<^command_keyword>\<open>syntax_types\<close> "declare syntax const dependencies (type names)"
+    (syntax_consts >> Isar_Cmd.syntax_types);
 
 val trans_pat =
   Scan.optional

--- a/src/Pure/Syntax/local_syntax.ML	Sat Dec 14 22:26:27 2024 +0100
+++ b/src/Pure/Syntax/local_syntax.ML	Sat Dec 14 23:48:45 2024 +0100
@@ -14,6 +14,7 @@
   datatype kind = Type | Const | Fixed
   val add_syntax: Proof.context -> (kind * (string * typ * mixfix)) list ->
     T -> {structs: string list, fixes: string list} option * T
+  val syntax_deps: Proof.context -> (string * string list) list -> T -> T
   val translations: Proof.context -> bool -> Ast.ast Syntax.trrule list -> T -> T
   val set_mode: Syntax.mode -> T -> T
   val restore_mode: T -> T -> T
@@ -36,14 +37,15 @@
   local_syntax: Syntax.syntax,
   mode: Syntax.mode,
   mixfixes: local_mixfix list,
+  consts: (string * string list) list,
   translations: (bool * Ast.ast Syntax.trrule list) list};
 
-fun make_syntax (thy_syntax, local_syntax, mode, mixfixes, translations) =
+fun make_syntax (thy_syntax, local_syntax, mode, mixfixes, consts, translations) =
   Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax, mode = mode,
-    mixfixes = mixfixes, translations = translations};
+    mixfixes = mixfixes, consts = consts, translations = translations};
 
-fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes, translations}) =
-  make_syntax (f (thy_syntax, local_syntax, mode, mixfixes, translations));
+fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes, consts, translations}) =
+  make_syntax (f (thy_syntax, local_syntax, mode, mixfixes, consts, translations));
 
 fun is_consistent ctxt (Syntax {thy_syntax, ...}) =
   Syntax.eq_syntax (Sign.syntax_of (Proof_Context.theory_of ctxt), thy_syntax);
@@ -53,7 +55,7 @@
 
 (* build syntax *)
 
-fun build_syntax ctxt mode mixfixes translations =
+fun build_syntax ctxt mode mixfixes consts translations =
   let
     val thy = Proof_Context.theory_of ctxt;
     val thy_syntax = Sign.syntax_of thy;
@@ -64,16 +66,17 @@
 
     val local_syntax = thy_syntax
       |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes)))
+      |> Syntax.update_consts ctxt consts
       |> fold_rev (uncurry (Syntax.update_trrules ctxt)) translations;
-  in make_syntax (thy_syntax, local_syntax, mode, mixfixes, translations) end;
+  in make_syntax (thy_syntax, local_syntax, mode, mixfixes, consts, translations) end;
 
 fun init thy =
   let val thy_syntax = Sign.syntax_of thy
-  in make_syntax (thy_syntax, thy_syntax, Syntax.mode_default, [], []) end;
+  in make_syntax (thy_syntax, thy_syntax, Syntax.mode_default, [], [], []) end;
 
-fun rebuild ctxt (syntax as Syntax {mode, mixfixes, translations, ...}) =
+fun rebuild ctxt (syntax as Syntax {mode, mixfixes, consts, translations, ...}) =
   if is_consistent ctxt syntax then syntax
-  else build_syntax ctxt mode mixfixes translations;
+  else build_syntax ctxt mode mixfixes consts translations;
 
 
 (* mixfix declarations *)
@@ -97,7 +100,7 @@
 
 in
 
-fun update_syntax ctxt add raw_decls (syntax as (Syntax {mode, mixfixes, translations, ...})) =
+fun update_syntax ctxt add raw_decls (syntax as (Syntax {mode, mixfixes, consts, translations, ...})) =
   (case filter_out (Mixfix.is_empty o #3 o #2) raw_decls of
     [] => (NONE, syntax)
   | decls =>
@@ -113,7 +116,7 @@
             else subtract (op =) new_structs (#structs idents),
            fixes = fold (fn ({name = x, is_fixed = true}, _) => cons x | _ => I) mixfixes' []};
 
-        val syntax' = build_syntax ctxt mode mixfixes' translations;
+        val syntax' = build_syntax ctxt mode mixfixes' consts translations;
       in (if idents = idents' then NONE else SOME idents', syntax') end);
 
 fun add_syntax ctxt = update_syntax ctxt true;
@@ -123,14 +126,18 @@
 
 (* translations *)
 
-fun translations ctxt add args (Syntax {thy_syntax, local_syntax, mode, mixfixes, translations}) =
-  (Sign.check_translations ctxt args; build_syntax ctxt mode mixfixes ((add, args) :: translations));
+fun syntax_deps ctxt args (Syntax {mode, mixfixes, consts, translations, ...}) =
+  build_syntax ctxt mode mixfixes (args @ consts) translations;
+
+fun translations ctxt add args (Syntax {mode, mixfixes, consts, translations, ...}) =
+ (Sign.check_translations ctxt args;
+  build_syntax ctxt mode mixfixes consts ((add, args) :: translations));
 
 
 (* syntax mode *)
 
-fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes, translations) =>
-  (thy_syntax, local_syntax, mode, mixfixes, translations));
+fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes, consts, translations) =>
+  (thy_syntax, local_syntax, mode, mixfixes, consts, translations));
 
 fun restore_mode (Syntax {mode, ...}) = set_mode mode;
 

--- a/src/Pure/sign.ML	Sat Dec 14 22:26:27 2024 +0100
+++ b/src/Pure/sign.ML	Sat Dec 14 23:48:45 2024 +0100
@@ -102,6 +102,7 @@
     (string * (Proof.context -> typ -> term list -> term)) list -> theory -> theory
   val print_ast_translation:
     (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory
+  val check_syntax_dep: Proof.context -> string -> unit
   val check_translations: Proof.context -> Ast.ast Syntax.trrule list -> unit
   val translations: Proof.context -> bool -> Ast.ast Syntax.trrule list -> theory -> theory
   val translations_global: bool -> Ast.ast Syntax.trrule list -> theory -> theory
@@ -520,26 +521,27 @@
 
 (* translation rules *)
 
-fun check_translations ctxt =
+fun check_syntax_dep ctxt s =
   let
     val thy = Proof_Context.theory_of ctxt;
-
-    fun err msg = error ("Malformed syntax translations: " ^ msg);
+    fun print_type c = uncurry Markup.markup (Name_Space.markup_extern ctxt (type_space thy) c);
+    fun print_const c = uncurry Markup.markup (Name_Space.markup_extern ctxt (const_space thy) c);
+  in
+    s |> Lexicon.unmark
+     {case_class = K (),
+      case_type = fn c =>
+        if declared_tyname thy c then () else error ("Not a global type: " ^ quote (print_type c)),
+      case_const = fn c =>
+        if declared_const thy c then () else error ("Not a global const: " ^ quote (print_const c)),
+      case_fixed = fn x => error ("Bad local variable: " ^ quote x),
+      case_default = K ()}
+  end;
 
-    fun print_const c =
-      uncurry Markup.markup (Name_Space.markup_extern ctxt (const_space thy) c);
-
+fun check_translations ctxt =
+  let
     fun check_ast (Ast.Appl asts) = List.app check_ast asts
       | check_ast (Ast.Variable _) = ()
-      | check_ast (Ast.Constant s) =
-          (case try Lexicon.unmark_fixed s of
-            NONE =>
-              (case try Lexicon.unmark_const s of
-                SOME c =>
-                  if declared_const thy c then ()
-                  else err ("non-global constant " ^ quote (print_const c))
-              | NONE => ())
-          | SOME x => err ("local variable " ^ Syntax.string_of_term ctxt (Syntax.free x)));
+      | check_ast (Ast.Constant s) = check_syntax_dep ctxt s;
   in List.app (ignore o Syntax.map_trrule (tap check_ast)) end;
 
 fun translations ctxt add args thy =