localized command 'syntax' and 'no_syntax';

--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Mon Sep 20 21:56:10 2021 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Mon Sep 20 23:15:02 2021 +0200
@@ -1077,8 +1077,8 @@
 text \<open>
   \begin{tabular}{rcll}
     @{command_def "nonterminal"} & : & \<open>theory \<rightarrow> theory\<close> \\
-    @{command_def "syntax"} & : & \<open>theory \<rightarrow> theory\<close> \\
-    @{command_def "no_syntax"} & : & \<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 "translations"} & : & \<open>theory \<rightarrow> theory\<close> \\
     @{command_def "no_translations"} & : & \<open>theory \<rightarrow> theory\<close> \\
     @{attribute_def syntax_ast_trace} & : & \<open>attribute\<close> & default \<open>false\<close> \\

--- a/src/Pure/Isar/local_theory.ML	Mon Sep 20 21:56:10 2021 +0200
+++ b/src/Pure/Isar/local_theory.ML	Mon Sep 20 23:15:02 2021 +0200
@@ -60,6 +60,10 @@
   val pretty: local_theory -> Pretty.T list
   val add_thms_dynamic: binding * (Context.generic -> thm list) -> local_theory -> local_theory
   val set_defsort: sort -> local_theory -> local_theory
+  val syntax: bool -> Syntax.mode -> (string * typ * mixfix) list ->
+    local_theory -> local_theory
+  val syntax_cmd: bool -> Syntax.mode -> (string * string * mixfix) list ->
+    local_theory -> local_theory
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val type_alias: binding -> string -> local_theory -> local_theory
@@ -297,6 +301,22 @@
     (K (Context.mapping (Sign.set_defsort S) (Proof_Context.set_defsort S)));
 
 
+(* syntax *)
+
+fun gen_syntax prep_type add mode raw_args lthy =
+  let
+    val args = map (fn (c, T, mx) => (c, prep_type lthy T, mx)) raw_args;
+    val args' = map (fn (c, T, mx) => (c, T, Mixfix.reset_pos mx)) args;
+    val _ = lthy |> Context_Position.is_visible lthy ? Proof_Context.syntax add mode args;
+  in
+    declaration {syntax = true, pervasive = false}
+      (fn _ => Proof_Context.generic_syntax add mode args') lthy
+  end;
+
+val syntax = gen_syntax (K I);
+val syntax_cmd = gen_syntax Proof_Context.read_typ_syntax;
+
+
 (* notation *)
 
 fun type_notation add mode raw_args lthy =

--- a/src/Pure/Isar/proof_context.ML	Mon Sep 20 21:56:10 2021 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Sep 20 23:15:02 2021 +0200
@@ -156,6 +156,10 @@
   val check_case: Proof.context -> bool ->
     string * Position.T -> binding option list -> Rule_Cases.T
   val check_syntax_const: Proof.context -> string * Position.T -> string
+  val syntax: bool -> Syntax.mode -> (string * typ * mixfix) list ->
+    Proof.context -> Proof.context
+  val generic_syntax: bool -> Syntax.mode -> (string * typ * mixfix) list ->
+    Context.generic -> Context.generic
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> Proof.context -> Proof.context
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context
   val generic_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism ->
@@ -1130,6 +1134,13 @@
   if is_some (Syntax.lookup_const (syn_of ctxt) c) then c
   else error ("Unknown syntax const: " ^ quote c ^ Position.here pos);
 
+fun syntax add mode args ctxt =
+  let val args' = map (pair Local_Syntax.Const) args
+  in ctxt |> map_syntax (#2 o Local_Syntax.update_modesyntax ctxt add mode args') end;
+
+fun generic_syntax add mode args =
+  Context.mapping (Sign.syntax add mode args) (syntax add mode args);
+
 
 (* notation *)
 

--- a/src/Pure/Pure.thy	Mon Sep 20 21:56:10 2021 +0200
+++ b/src/Pure/Pure.thy	Mon Sep 20 23:15:02 2021 +0200
@@ -384,14 +384,14 @@
     (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));
 
 val _ =
-  Outer_Syntax.command \<^command_keyword>\<open>syntax\<close> "add raw syntax clauses"
+  Outer_Syntax.local_theory \<^command_keyword>\<open>syntax\<close> "add raw syntax clauses"
     (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl
-      >> (Toplevel.theory o uncurry (Sign.syntax_cmd true)));
+      >> uncurry (Local_Theory.syntax_cmd true));
 
 val _ =
-  Outer_Syntax.command \<^command_keyword>\<open>no_syntax\<close> "delete raw syntax clauses"
+  Outer_Syntax.local_theory \<^command_keyword>\<open>no_syntax\<close> "delete raw syntax clauses"
     (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl
-      >> (Toplevel.theory o uncurry (Sign.syntax_cmd false)));
+      >> uncurry (Local_Theory.syntax_cmd false));
 
 val trans_pat =
   Scan.optional