uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;

--- a/src/Pure/Isar/local_theory.ML	Thu Nov 23 20:33:36 2006 +0100
+++ b/src/Pure/Isar/local_theory.ML	Thu Nov 23 20:33:37 2006 +0100
@@ -27,8 +27,9 @@
     local_theory -> (term * (bstring * thm)) list * local_theory
   val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
     local_theory -> (bstring * thm list) list * local_theory
-  val term_syntax: (Context.generic -> Context.generic) -> local_theory -> local_theory
-  val declaration: (Context.generic -> Context.generic) -> local_theory -> local_theory
+  val type_syntax: (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory
+  val term_syntax: (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory
+  val declaration: (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory
   val def: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) ->
     local_theory -> (term * (bstring * thm)) * local_theory
   val note: string -> (bstring * Attrib.src list) * thm list ->
@@ -60,8 +61,9 @@
   notes: string ->
     ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
     local_theory -> (bstring * thm list) list * local_theory,
-  term_syntax: (Context.generic -> Context.generic) -> local_theory -> local_theory,
-  declaration: (Context.generic -> Context.generic) -> local_theory -> local_theory,
+  type_syntax: (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory,
+  term_syntax: (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory,
+  declaration: (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory,
   reinit: local_theory -> theory -> local_theory,
   exit: local_theory -> Proof.context};
 
@@ -147,6 +149,7 @@
 val axioms = operation2 #axioms;
 val defs = operation2 #defs;
 val notes = operation2 #notes;
+val type_syntax = operation1 #type_syntax;
 val term_syntax = operation1 #term_syntax;
 val declaration = operation1 #declaration;
 
@@ -157,11 +160,11 @@
 
 fun note kind (a, ths) lthy = lthy |> notes kind [(a, [(ths, [])])] |>> hd;
 
-fun notation mode args = term_syntax
-  (Context.mapping (Sign.add_notation mode args) (ProofContext.add_notation mode args));
+fun notation mode args = term_syntax (fn phi => (* FIXME *)
+  (Context.mapping (Sign.add_notation mode args) (ProofContext.add_notation mode args)));
 
-fun abbrevs mode args = term_syntax
-  (Context.mapping (snd o Sign.add_abbrevs mode args) (snd o ProofContext.add_abbrevs mode args))
+fun abbrevs mode args = term_syntax (fn phi => (* FIXME *)
+  (Context.mapping (snd o Sign.add_abbrevs mode args) (snd o ProofContext.add_abbrevs mode args)))
   #> ProofContext.add_abbrevs mode args;  (* FIXME *)
 
 

--- a/src/Pure/Isar/theory_target.ML	Thu Nov 23 20:33:36 2006 +0100
+++ b/src/Pure/Isar/theory_target.ML	Thu Nov 23 20:33:37 2006 +0100
@@ -198,11 +198,13 @@
 
 (* declarations *)
 
-fun term_syntax "" f = LocalTheory.theory (Context.theory_map f)
-  | term_syntax loc f = LocalTheory.target (Locale.add_term_syntax loc (Context.proof_map f));
+(* FIXME proper morphisms *)
+fun decl _ "" f = LocalTheory.theory (Context.theory_map (f Morphism.identity))
+  | decl add loc f = LocalTheory.target (add loc (Context.proof_map o f));
 
-fun declaration "" f = LocalTheory.theory (Context.theory_map f)
-  | declaration loc f = I;    (* FIXME *)
+val type_syntax = decl Locale.add_type_syntax;
+val term_syntax = decl Locale.add_term_syntax;
+val declaration = decl Locale.add_declaration;
 
 
 (* init and exit *)
@@ -215,6 +217,7 @@
     axioms = axioms,
     defs = defs,
     notes = notes loc,
+    type_syntax = type_syntax loc,
     term_syntax = term_syntax loc,
     declaration = declaration loc,
     reinit = fn _ => begin loc o (if loc = "" then ProofContext.init else Locale.init loc),