25 val global_target = Target {target = "", is_locale = false, is_class = false}; |
25 val global_target = Target {target = "", is_locale = false, is_class = false}; |
26 |
26 |
27 fun named_target _ NONE = global_target |
27 fun named_target _ NONE = global_target |
28 | named_target thy (SOME locale) = |
28 | named_target thy (SOME locale) = |
29 if Locale.defined thy locale |
29 if Locale.defined thy locale |
30 then Target {target = locale, is_locale = true, is_class = Class_Target.is_class thy locale} |
30 then Target {target = locale, is_locale = true, is_class = Class.is_class thy locale} |
31 else error ("No such locale: " ^ quote locale); |
31 else error ("No such locale: " ^ quote locale); |
32 |
32 |
33 structure Data = Proof_Data |
33 structure Data = Proof_Data |
34 ( |
34 ( |
35 type T = target; |
35 type T = target; |
67 (* FIXME workaround based on educated guess *) |
67 (* FIXME workaround based on educated guess *) |
68 val prefix' = Binding.prefix_of b'; |
68 val prefix' = Binding.prefix_of b'; |
69 val is_canonical_class = is_class andalso |
69 val is_canonical_class = is_class andalso |
70 (Binding.eq_name (b, b') |
70 (Binding.eq_name (b, b') |
71 andalso not (null prefix') |
71 andalso not (null prefix') |
72 andalso List.last prefix' = (Class_Target.class_prefix target, false) |
72 andalso List.last prefix' = (Class.class_prefix target, false) |
73 orelse same_shape); |
73 orelse same_shape); |
74 in |
74 in |
75 not is_canonical_class ? |
75 not is_canonical_class ? |
76 (Context.mapping_result |
76 (Context.mapping_result |
77 (Sign.add_abbrev Print_Mode.internal arg) |
77 (Sign.add_abbrev Print_Mode.internal arg) |
86 fun locale_const_declaration (ta as Target {target, ...}) prmode arg = |
86 fun locale_const_declaration (ta as Target {target, ...}) prmode arg = |
87 locale_declaration target { syntax = true, pervasive = false } (locale_const ta prmode arg); |
87 locale_declaration target { syntax = true, pervasive = false } (locale_const ta prmode arg); |
88 |
88 |
89 fun class_target (Target {target, ...}) f = |
89 fun class_target (Target {target, ...}) f = |
90 Local_Theory.raw_theory f #> |
90 Local_Theory.raw_theory f #> |
91 Local_Theory.target (Class_Target.refresh_syntax target); |
91 Local_Theory.target (Class.refresh_syntax target); |
92 |
92 |
93 |
93 |
94 (* define *) |
94 (* define *) |
95 |
95 |
96 fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) = |
96 fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) = |
100 |
100 |
101 fun class_foundation (ta as Target {target, ...}) |
101 fun class_foundation (ta as Target {target, ...}) |
102 (((b, U), mx), (b_def, rhs)) (type_params, term_params) = |
102 (((b, U), mx), (b_def, rhs)) (type_params, term_params) = |
103 Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params) |
103 Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params) |
104 #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs) |
104 #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs) |
105 #> class_target ta (Class_Target.declare target ((b, mx), (type_params, lhs))) |
105 #> class_target ta (Class.declare target ((b, mx), (type_params, lhs))) |
106 #> pair (lhs, def)) |
106 #> pair (lhs, def)) |
107 |
107 |
108 fun target_foundation (ta as Target {target, is_locale, is_class, ...}) = |
108 fun target_foundation (ta as Target {target, is_locale, is_class, ...}) = |
109 if is_class then class_foundation ta |
109 if is_class then class_foundation ta |
110 else if is_locale then locale_foundation ta |
110 else if is_locale then locale_foundation ta |
139 fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) |
139 fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) |
140 prmode (b, mx) (global_rhs, t') xs lthy = |
140 prmode (b, mx) (global_rhs, t') xs lthy = |
141 if is_locale |
141 if is_locale |
142 then lthy |
142 then lthy |
143 |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs |
143 |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs |
144 |> is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx), t')) |
144 |> is_class ? class_target ta (Class.abbrev target prmode ((b, mx), t')) |
145 else lthy |
145 else lthy |
146 |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs); |
146 |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs); |
147 |
147 |
148 |
148 |
149 (* pretty *) |
149 (* pretty *) |
179 local |
179 local |
180 |
180 |
181 fun init_context (Target {target, is_locale, is_class}) = |
181 fun init_context (Target {target, is_locale, is_class}) = |
182 if not is_locale then ProofContext.init_global |
182 if not is_locale then ProofContext.init_global |
183 else if not is_class then Locale.init target |
183 else if not is_class then Locale.init target |
184 else Class_Target.init target; |
184 else Class.init target; |
185 |
185 |
186 fun init_target (ta as Target {target, ...}) thy = |
186 fun init_target (ta as Target {target, ...}) thy = |
187 thy |
187 thy |
188 |> init_context ta |
188 |> init_context ta |
189 |> Data.put ta |
189 |> Data.put ta |