1.1 --- a/src/Pure/Isar/theory_target.ML Fri Dec 12 15:02:15 2008 +0100
1.2 +++ b/src/Pure/Isar/theory_target.ML Fri Dec 12 17:00:42 2008 +0100
1.3 @@ -8,7 +8,7 @@
1.4
1.5 signature THEORY_TARGET =
1.6 sig
1.7 - val peek: local_theory -> {target: string, is_locale: bool,
1.8 + val peek: local_theory -> {target: string, new_locale: bool, is_locale: bool,
1.9 is_class: bool, instantiation: string list * (string * sort) list * sort,
1.10 overloading: (string * (string * typ) * bool) list}
1.11 val init: string option -> theory -> local_theory
1.12 @@ -24,32 +24,32 @@
1.13
1.14 (* new locales *)
1.15
1.16 -fun locale_extern is_class x =
1.17 - if !new_locales andalso not is_class then NewLocale.extern x else Locale.extern x;
1.18 -fun locale_add_type_syntax is_class x =
1.19 - if !new_locales andalso not is_class then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
1.20 -fun locale_add_term_syntax is_class x =
1.21 - if !new_locales andalso not is_class then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
1.22 -fun locale_add_declaration is_class x =
1.23 - if !new_locales andalso not is_class then NewLocale.add_declaration x else Locale.add_declaration x;
1.24 -fun locale_add_thmss is_class x =
1.25 - if !new_locales andalso not is_class then NewLocale.add_thmss x else Locale.add_thmss x;
1.26 -fun locale_init x =
1.27 - if !new_locales then NewLocale.init x else Locale.init x;
1.28 -fun locale_intern is_class x =
1.29 - if !new_locales andalso not is_class then NewLocale.intern x else Locale.intern x;
1.30 +fun locale_extern new_locale x =
1.31 + if !new_locales andalso new_locale then NewLocale.extern x else Locale.extern x;
1.32 +fun locale_add_type_syntax new_locale x =
1.33 + if !new_locales andalso new_locale then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
1.34 +fun locale_add_term_syntax new_locale x =
1.35 + if !new_locales andalso new_locale then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
1.36 +fun locale_add_declaration new_locale x =
1.37 + if !new_locales andalso new_locale then NewLocale.add_declaration x else Locale.add_declaration x;
1.38 +fun locale_add_thmss new_locale x =
1.39 + if !new_locales andalso new_locale then NewLocale.add_thmss x else Locale.add_thmss x;
1.40 +fun locale_init new_locale x =
1.41 + if !new_locales andalso new_locale then NewLocale.init x else Locale.init x;
1.42 +fun locale_intern new_locale x =
1.43 + if !new_locales andalso new_locale then NewLocale.intern x else Locale.intern x;
1.44
1.45 (* context data *)
1.46
1.47 -datatype target = Target of {target: string, is_locale: bool,
1.48 +datatype target = Target of {target: string, new_locale: bool, is_locale: bool,
1.49 is_class: bool, instantiation: string list * (string * sort) list * sort,
1.50 overloading: (string * (string * typ) * bool) list};
1.51
1.52 -fun make_target target is_locale is_class instantiation overloading =
1.53 - Target {target = target, is_locale = is_locale,
1.54 +fun make_target target new_locale is_locale is_class instantiation overloading =
1.55 + Target {target = target, new_locale = new_locale, is_locale = is_locale,
1.56 is_class = is_class, instantiation = instantiation, overloading = overloading};
1.57
1.58 -val global_target = make_target "" false false ([], [], []) [];
1.59 +val global_target = make_target "" false false false ([], [], []) [];
1.60
1.61 structure Data = ProofDataFun
1.62 (
1.63 @@ -80,7 +80,7 @@
1.64 (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)]
1.65 end;
1.66
1.67 -fun pretty (Target {target, is_locale, is_class, instantiation, overloading}) ctxt =
1.68 +fun pretty (Target {target, is_locale, is_class, instantiation, overloading, ...}) ctxt =
1.69 Pretty.block [Pretty.str "theory", Pretty.brk 1,
1.70 Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] ::
1.71 (if not (null overloading) then [Overloading.pretty ctxt]
1.72 @@ -90,7 +90,7 @@
1.73
1.74 (* target declarations *)
1.75
1.76 -fun target_decl add (Target {target, is_class, ...}) d lthy =
1.77 +fun target_decl add (Target {target, new_locale, ...}) d lthy =
1.78 let
1.79 val d' = Morphism.transform (LocalTheory.target_morphism lthy) d;
1.80 val d0 = Morphism.form d';
1.81 @@ -101,7 +101,7 @@
1.82 |> LocalTheory.target (Context.proof_map d0)
1.83 else
1.84 lthy
1.85 - |> LocalTheory.target (add is_class target d')
1.86 + |> LocalTheory.target (add new_locale target d')
1.87 end;
1.88
1.89 val type_syntax = target_decl locale_add_type_syntax;
1.90 @@ -167,7 +167,7 @@
1.91 |> ProofContext.note_thmss_i kind facts
1.92 ||> ProofContext.restore_naming ctxt;
1.93
1.94 -fun notes (Target {target, is_locale, is_class, ...}) kind facts lthy =
1.95 +fun notes (Target {target, is_locale, new_locale, ...}) kind facts lthy =
1.96 let
1.97 val thy = ProofContext.theory_of lthy;
1.98 val facts' = facts
1.99 @@ -186,7 +186,7 @@
1.100 #> PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd
1.101 #> Sign.restore_naming thy)
1.102 |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd)
1.103 - |> is_locale ? LocalTheory.target (locale_add_thmss is_class target kind target_facts)
1.104 + |> is_locale ? LocalTheory.target (locale_add_thmss new_locale target kind target_facts)
1.105 |> note_local kind local_facts
1.106 end;
1.107
1.108 @@ -335,13 +335,14 @@
1.109
1.110 fun init_target _ NONE = global_target
1.111 | init_target thy (SOME target) =
1.112 - make_target target true (Class.is_class thy target) ([], [], []) [];
1.113 + make_target target (NewLocale.test_locale thy (NewLocale.intern thy target))
1.114 + true (Class.is_class thy target) ([], [], []) [];
1.115
1.116 -fun init_ctxt (Target {target, is_locale, is_class, instantiation, overloading}) =
1.117 +fun init_ctxt (Target {target, new_locale, is_locale, is_class, instantiation, overloading}) =
1.118 if not (null (#1 instantiation)) then Class.init_instantiation instantiation
1.119 else if not (null overloading) then Overloading.init overloading
1.120 else if not is_locale then ProofContext.init
1.121 - else if not is_class then locale_init target
1.122 + else if not is_class then locale_init new_locale target
1.123 else Class.init target;
1.124
1.125 fun init_lthy (ta as Target {target, instantiation, overloading, ...}) =
1.126 @@ -366,7 +367,7 @@
1.127 val ctxt = ProofContext.init thy;
1.128 val ops = raw_ops |> map (fn (name, const, checked) =>
1.129 (name, Term.dest_Const (prep_const ctxt const), checked));
1.130 - in thy |> init_lthy_ctxt (make_target "" false false ([], [], []) ops) end;
1.131 + in thy |> init_lthy_ctxt (make_target "" false false false ([], [], []) ops) end;
1.132
1.133 in
1.134
1.135 @@ -375,9 +376,9 @@
1.136
1.137 fun context "-" thy = init NONE thy
1.138 | context target thy = init (SOME (locale_intern
1.139 - (not (NewLocale.test_locale thy (NewLocale.intern thy target))) thy target)) thy;
1.140 + (NewLocale.test_locale thy (NewLocale.intern thy target)) thy target)) thy;
1.141
1.142 -fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []);
1.143 +fun instantiation arities = init_lthy_ctxt (make_target "" false false false arities []);
1.144
1.145 val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
1.146 val overloading_cmd = gen_overloading Syntax.read_term;