author | wenzelm |
Wed, 29 Dec 2010 17:34:41 +0100 | |
changeset 41413 | 64cd30d6b0b8 |
parent 40782 | aa533c5e3f48 |
child 41585 | 45d7da4e4ccf |
permissions | -rw-r--r-- |
20894 | 1 |
(* Title: Pure/Isar/theory_target.ML |
2 |
Author: Makarius |
|
30437 | 3 |
Author: Florian Haftmann, TU Muenchen |
20894 | 4 |
|
38350
480b2de9927c
renamed Theory_Target to the more appropriate Named_Target
haftmann
parents:
38349
diff
changeset
|
5 |
Targets for theory, locale and class. |
20894 | 6 |
*) |
7 |
||
38350
480b2de9927c
renamed Theory_Target to the more appropriate Named_Target
haftmann
parents:
38349
diff
changeset
|
8 |
signature NAMED_TARGET = |
20894 | 9 |
sig |
38389
d7d915bae307
Named_Target.init: empty string represents theory target
haftmann
parents:
38388
diff
changeset
|
10 |
val init: string -> theory -> local_theory |
38388 | 11 |
val theory_init: theory -> local_theory |
38391
ba1cc1815ce1
named target is optional; explicit Name_Target.reinit
haftmann
parents:
38389
diff
changeset
|
12 |
val reinit: local_theory -> local_theory -> local_theory |
35205 | 13 |
val context_cmd: xstring -> theory -> local_theory |
38391
ba1cc1815ce1
named target is optional; explicit Name_Target.reinit
haftmann
parents:
38389
diff
changeset
|
14 |
val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option |
20894 | 15 |
end; |
16 |
||
38350
480b2de9927c
renamed Theory_Target to the more appropriate Named_Target
haftmann
parents:
38349
diff
changeset
|
17 |
structure Named_Target: NAMED_TARGET = |
20894 | 18 |
struct |
19 |
||
21006 | 20 |
(* context data *) |
21 |
||
38338
0e0e1fd9cc03
remove overloading and instantiation from data slot
haftmann
parents:
38319
diff
changeset
|
22 |
datatype target = Target of {target: string, is_locale: bool, is_class: bool}; |
25012
448af76a1ba3
pass explicit target record -- more informative peek operation;
wenzelm
parents:
25002
diff
changeset
|
23 |
|
39639 | 24 |
fun named_target _ "" = Target {target = "", is_locale = false, is_class = false} |
38389
d7d915bae307
Named_Target.init: empty string represents theory target
haftmann
parents:
38388
diff
changeset
|
25 |
| named_target thy locale = |
38378 | 26 |
if Locale.defined thy locale |
38379
67d71449e85b
more convenient split of class modules: class and class_declaration
haftmann
parents:
38378
diff
changeset
|
27 |
then Target {target = locale, is_locale = true, is_class = Class.is_class thy locale} |
38378 | 28 |
else error ("No such locale: " ^ quote locale); |
25012
448af76a1ba3
pass explicit target record -- more informative peek operation;
wenzelm
parents:
25002
diff
changeset
|
29 |
|
33519 | 30 |
structure Data = Proof_Data |
21006 | 31 |
( |
38391
ba1cc1815ce1
named target is optional; explicit Name_Target.reinit
haftmann
parents:
38389
diff
changeset
|
32 |
type T = target option; |
ba1cc1815ce1
named target is optional; explicit Name_Target.reinit
haftmann
parents:
38389
diff
changeset
|
33 |
fun init _ = NONE; |
21006 | 34 |
); |
35 |
||
38391
ba1cc1815ce1
named target is optional; explicit Name_Target.reinit
haftmann
parents:
38389
diff
changeset
|
36 |
val peek = Option.map (fn Target args => args) o Data.get; |
21006 | 37 |
|
38 |
||
33456
fbd47f9b9b12
allow "pervasive" local theory declarations, which are applied the background theory;
wenzelm
parents:
33282
diff
changeset
|
39 |
(* generic declarations *) |
fbd47f9b9b12
allow "pervasive" local theory declarations, which are applied the background theory;
wenzelm
parents:
33282
diff
changeset
|
40 |
|
40782 | 41 |
fun locale_declaration locale {syntax, pervasive} decl lthy = |
24838 | 42 |
let |
38305 | 43 |
val add = if syntax then Locale.add_syntax_declaration else Locale.add_declaration; |
44 |
val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl; |
|
24838 | 45 |
in |
38305 | 46 |
lthy |
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38339
diff
changeset
|
47 |
|> pervasive ? Generic_Target.theory_declaration decl |
38305 | 48 |
|> Local_Theory.target (add locale locale_decl) |
24838 | 49 |
end; |
50 |
||
40782 | 51 |
fun target_declaration (Target {target, ...}) {syntax, pervasive} = |
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38339
diff
changeset
|
52 |
if target = "" then Generic_Target.theory_declaration |
40782 | 53 |
else locale_declaration target {syntax = syntax, pervasive = pervasive}; |
24838 | 54 |
|
21611
fc95ff1fe738
notes: proper import/export of proofs (still inactive);
wenzelm
parents:
21594
diff
changeset
|
55 |
|
38297 | 56 |
(* consts in locales *) |
57 |
||
58 |
fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) phi = |
|
59 |
let |
|
60 |
val b' = Morphism.binding phi b; |
|
61 |
val rhs' = Morphism.term phi rhs; |
|
62 |
val arg = (b', Term.close_schematic_term rhs'); |
|
63 |
val same_shape = Term.aconv_untyped (rhs, rhs'); |
|
64 |
(* FIXME workaround based on educated guess *) |
|
65 |
val prefix' = Binding.prefix_of b'; |
|
66 |
val is_canonical_class = is_class andalso |
|
67 |
(Binding.eq_name (b, b') |
|
68 |
andalso not (null prefix') |
|
38379
67d71449e85b
more convenient split of class modules: class and class_declaration
haftmann
parents:
38378
diff
changeset
|
69 |
andalso List.last prefix' = (Class.class_prefix target, false) |
38297 | 70 |
orelse same_shape); |
71 |
in |
|
72 |
not is_canonical_class ? |
|
73 |
(Context.mapping_result |
|
74 |
(Sign.add_abbrev Print_Mode.internal arg) |
|
75 |
(ProofContext.add_abbrev Print_Mode.internal arg) |
|
76 |
#-> (fn (lhs' as Const (d, _), _) => |
|
77 |
same_shape ? |
|
38310 | 78 |
(Context.mapping |
79 |
(Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #> |
|
38297 | 80 |
Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)])))) |
81 |
end; |
|
82 |
||
38305 | 83 |
fun locale_const_declaration (ta as Target {target, ...}) prmode arg = |
40782 | 84 |
locale_declaration target {syntax = true, pervasive = false} (locale_const ta prmode arg); |
38305 | 85 |
|
38297 | 86 |
|
38318
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
87 |
(* define *) |
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
88 |
|
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
89 |
fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) = |
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38339
diff
changeset
|
90 |
Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params) |
38318
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
91 |
#-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, mx), lhs) |
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
92 |
#> pair (lhs, def)) |
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
93 |
|
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
94 |
fun class_foundation (ta as Target {target, ...}) |
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
95 |
(((b, U), mx), (b_def, rhs)) (type_params, term_params) = |
38341
72dba5bd5f63
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38339
diff
changeset
|
96 |
Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params) |
38318
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
97 |
#-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs) |
38619
25e401d53900
tuned: less formal noise in Named_Target, more coherence in Class
haftmann
parents:
38392
diff
changeset
|
98 |
#> Class.const target ((b, mx), (type_params, lhs)) |
38318
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
99 |
#> pair (lhs, def)) |
1fade69519ab
different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents:
38314
diff
changeset
|
100 |
|
39639 | 101 |
fun target_foundation (ta as Target {is_locale, is_class, ...}) = |
38349 | 102 |
if is_class then class_foundation ta |
103 |
else if is_locale then locale_foundation ta |
|
104 |
else Generic_Target.theory_foundation; |
|
38303
ad4b59e9d0f9
factored out foundation of `define` into separate function
haftmann
parents:
38302
diff
changeset
|
105 |
|
24939 | 106 |
|
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
107 |
(* notes *) |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
108 |
|
40782 | 109 |
fun locale_notes locale kind global_facts local_facts lthy = |
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
110 |
let |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
111 |
val global_facts' = Attrib.map_facts (K I) global_facts; |
38310 | 112 |
val local_facts' = Element.facts_map |
113 |
(Element.morph_ctxt (Local_Theory.target_morphism lthy)) local_facts; |
|
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
114 |
in |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
115 |
lthy |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
38757
diff
changeset
|
116 |
|> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd) |
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
117 |
|> Local_Theory.target (Locale.add_thmss locale kind local_facts') |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
118 |
end |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
119 |
|
39639 | 120 |
fun target_notes (Target {target, is_locale, ...}) = |
38319
1cfc2b128e33
separate initialisation for overloading and instantiation target
haftmann
parents:
38318
diff
changeset
|
121 |
if is_locale then locale_notes target |
40782 | 122 |
else fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts; |
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
123 |
|
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
124 |
|
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
125 |
(* abbrev *) |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
126 |
|
38757
2b3e054ae6fc
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38619
diff
changeset
|
127 |
fun locale_abbrev ta prmode ((b, mx), t) xs = |
2b3e054ae6fc
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38619
diff
changeset
|
128 |
Local_Theory.background_theory_result |
2b3e054ae6fc
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38619
diff
changeset
|
129 |
(Sign.add_abbrev Print_Mode.internal (b, t)) #-> |
2b3e054ae6fc
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38619
diff
changeset
|
130 |
(fn (lhs, _) => locale_const_declaration ta prmode |
2b3e054ae6fc
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38619
diff
changeset
|
131 |
((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs))); |
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
132 |
|
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
133 |
fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) |
38312
9dd57db3c0f2
moved extra_tfrees check for mixfix syntax to Generic_Target
haftmann
parents:
38311
diff
changeset
|
134 |
prmode (b, mx) (global_rhs, t') xs lthy = |
38757
2b3e054ae6fc
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38619
diff
changeset
|
135 |
if is_locale then |
2b3e054ae6fc
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38619
diff
changeset
|
136 |
lthy |
2b3e054ae6fc
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38619
diff
changeset
|
137 |
|> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs |
2b3e054ae6fc
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38619
diff
changeset
|
138 |
|> is_class ? Class.abbrev target prmode ((b, mx), t') |
2b3e054ae6fc
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38619
diff
changeset
|
139 |
else |
2b3e054ae6fc
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38619
diff
changeset
|
140 |
lthy |
2b3e054ae6fc
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38619
diff
changeset
|
141 |
|> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs); |
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
142 |
|
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
143 |
|
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
144 |
(* pretty *) |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
145 |
|
39639 | 146 |
fun pretty (Target {target, is_locale, is_class, ...}) ctxt = |
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
147 |
let |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
148 |
val thy = ProofContext.theory_of ctxt; |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
149 |
val target_name = |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
150 |
[Pretty.command (if is_class then "class" else "locale"), |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
151 |
Pretty.str (" " ^ Locale.extern thy target)]; |
38310 | 152 |
val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) |
153 |
(#1 (ProofContext.inferred_fixes ctxt)); |
|
154 |
val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])])) |
|
155 |
(Assumption.all_assms_of ctxt); |
|
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
156 |
val elems = |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
157 |
(if null fixes then [] else [Element.Fixes fixes]) @ |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
158 |
(if null assumes then [] else [Element.Assumes assumes]); |
40782 | 159 |
val body_elems = |
160 |
if not is_locale then [] |
|
39639 | 161 |
else if null elems then [Pretty.block target_name] |
162 |
else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) :: |
|
40782 | 163 |
map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))]; |
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
164 |
in |
39639 | 165 |
Pretty.block [Pretty.command "theory", Pretty.brk 1, |
166 |
Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] :: body_elems |
|
38308
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
167 |
end; |
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
168 |
|
0e4649095739
try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents:
38307
diff
changeset
|
169 |
|
38378 | 170 |
(* init *) |
25291 | 171 |
|
38378 | 172 |
fun init_context (Target {target, is_locale, is_class}) = |
38338
0e0e1fd9cc03
remove overloading and instantiation from data slot
haftmann
parents:
38319
diff
changeset
|
173 |
if not is_locale then ProofContext.init_global |
29576 | 174 |
else if not is_class then Locale.init target |
38379
67d71449e85b
more convenient split of class modules: class and class_declaration
haftmann
parents:
38378
diff
changeset
|
175 |
else Class.init target; |
25269 | 176 |
|
39639 | 177 |
fun init target thy = |
178 |
let |
|
179 |
val ta = named_target thy target; |
|
180 |
in |
|
181 |
thy |
|
182 |
|> init_context ta |
|
183 |
|> Data.put (SOME ta) |
|
184 |
|> Local_Theory.init NONE (Long_Name.base_name target) |
|
185 |
{define = Generic_Target.define (target_foundation ta), |
|
186 |
notes = Generic_Target.notes (target_notes ta), |
|
187 |
abbrev = Generic_Target.abbrev (target_abbrev ta), |
|
188 |
declaration = fn pervasive => target_declaration ta |
|
40782 | 189 |
{syntax = false, pervasive = pervasive}, |
39639 | 190 |
syntax_declaration = fn pervasive => target_declaration ta |
40782 | 191 |
{syntax = true, pervasive = pervasive}, |
39639 | 192 |
pretty = pretty ta, |
193 |
exit = Local_Theory.target_of} |
|
194 |
end; |
|
38247 | 195 |
|
39639 | 196 |
val theory_init = init ""; |
25269 | 197 |
|
38757
2b3e054ae6fc
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38619
diff
changeset
|
198 |
fun reinit lthy = |
2b3e054ae6fc
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38619
diff
changeset
|
199 |
(case peek lthy of |
2b3e054ae6fc
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38619
diff
changeset
|
200 |
SOME {target, ...} => init target o Local_Theory.exit_global |
2b3e054ae6fc
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38619
diff
changeset
|
201 |
| NONE => error "Not in a named target"); |
38391
ba1cc1815ce1
named target is optional; explicit Name_Target.reinit
haftmann
parents:
38389
diff
changeset
|
202 |
|
38389
d7d915bae307
Named_Target.init: empty string represents theory target
haftmann
parents:
38388
diff
changeset
|
203 |
fun context_cmd "-" thy = init "" thy |
d7d915bae307
Named_Target.init: empty string represents theory target
haftmann
parents:
38388
diff
changeset
|
204 |
| context_cmd target thy = init (Locale.intern thy target) thy; |
33282 | 205 |
|
20894 | 206 |
end; |