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),