equal
deleted
inserted
replaced
7 |
7 |
8 signature NAMED_TARGET = |
8 signature NAMED_TARGET = |
9 sig |
9 sig |
10 val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} |
10 val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} |
11 val init: string option -> theory -> local_theory |
11 val init: string option -> theory -> local_theory |
|
12 val theory_init: theory -> local_theory |
12 val context_cmd: xstring -> theory -> local_theory |
13 val context_cmd: xstring -> theory -> local_theory |
13 end; |
14 end; |
14 |
15 |
15 structure Named_Target: NAMED_TARGET = |
16 structure Named_Target: NAMED_TARGET = |
16 struct |
17 struct |
200 |
201 |
201 in |
202 in |
202 |
203 |
203 fun init target thy = init_target (named_target thy target) thy; |
204 fun init target thy = init_target (named_target thy target) thy; |
204 |
205 |
|
206 val theory_init = init_target global_target; |
|
207 |
205 fun context_cmd "-" thy = init NONE thy |
208 fun context_cmd "-" thy = init NONE thy |
206 | context_cmd target thy = init (SOME (Locale.intern thy target)) thy; |
209 | context_cmd target thy = init (SOME (Locale.intern thy target)) thy; |
207 |
210 |
208 end; |
211 end; |
209 |
212 |