# HG changeset patch
# User wenzelm
# Date 1147807991 -7200
# Node ID e3ec6839c631222c6cf54cedf8e42b56be775646
# Parent  88d246e5f4bdff7a094b9444040c67e3396b6833
added add_modesyntax;
tuned;

diff -r 88d246e5f4bd -r e3ec6839c631 src/Pure/Isar/local_syntax.ML
--- a/src/Pure/Isar/local_syntax.ML	Tue May 16 21:33:09 2006 +0200
+++ b/src/Pure/Isar/local_syntax.ML	Tue May 16 21:33:11 2006 +0200
@@ -14,9 +14,10 @@
   val structs_of: T -> string list
   val init: theory -> T
   val rebuild: theory -> T -> T
+  val add_syntax: theory -> (bool * (string * typ * mixfix)) list -> T -> T
   val set_mode: string * bool -> T -> T
   val restore_mode: T -> T -> T
-  val add_syntax: theory -> (bool * (string * typ * mixfix)) list -> T -> T
+  val add_modesyntax: theory -> string * bool -> (bool * (string * typ * mixfix)) list -> T -> T
   val extern_term: T -> term -> term
 end;
 
@@ -73,14 +74,6 @@
   else build_syntax thy mode mixfixes idents;
 
 
-(* syntax mode *)
-
-fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes, idents) =>
-  (thy_syntax, local_syntax, mode, mixfixes, idents));
-
-fun restore_mode (Syntax {mode, ...}) = set_mode mode;
-
-
 (* mixfix declarations *)
 
 local
@@ -120,6 +113,17 @@
 end;
 
 
+(* syntax mode *)
+
+fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes, idents) =>
+  (thy_syntax, local_syntax, mode, mixfixes, idents));
+
+fun restore_mode (Syntax {mode, ...}) = set_mode mode;
+
+fun add_modesyntax thy mode args syntax =
+  syntax |> set_mode mode |> add_syntax thy args |> restore_mode syntax;
+
+
 (* extern_term *)
 
 fun extern_term syntax =