9 sig |
9 sig |
10 val is_theory: local_theory -> bool |
10 val is_theory: local_theory -> bool |
11 val locale_of: local_theory -> string option |
11 val locale_of: local_theory -> string option |
12 val bottom_locale_of: local_theory -> string option |
12 val bottom_locale_of: local_theory -> string option |
13 val class_of: local_theory -> string option |
13 val class_of: local_theory -> string option |
14 val init: string -> theory -> local_theory |
14 val init: (local_theory -> local_theory) option -> string -> theory -> local_theory |
15 val theory_init: theory -> local_theory |
15 val theory_init: theory -> local_theory |
16 val theory_map: (local_theory -> local_theory) -> theory -> theory |
16 val theory_map: (local_theory -> local_theory) -> theory -> theory |
17 val theory_like_init: (local_theory -> local_theory) -> theory -> local_theory |
|
18 val begin: xstring * Position.T -> theory -> local_theory |
17 val begin: xstring * Position.T -> theory -> local_theory |
19 val exit: local_theory -> theory |
18 val exit: local_theory -> theory |
20 val switch: (xstring * Position.T) option -> Context.generic |
19 val switch: (xstring * Position.T) option -> Context.generic -> |
21 -> (local_theory -> Context.generic) * local_theory |
20 (local_theory -> Context.generic) * local_theory |
22 end; |
21 end; |
23 |
22 |
24 structure Named_Target: NAMED_TARGET = |
23 structure Named_Target: NAMED_TARGET = |
25 struct |
24 struct |
26 |
25 |
131 |
130 |
132 fun init_context ("", _) = Proof_Context.init_global |
131 fun init_context ("", _) = Proof_Context.init_global |
133 | init_context (locale, false) = Locale.init locale |
132 | init_context (locale, false) = Locale.init locale |
134 | init_context (class, true) = Class.init class; |
133 | init_context (class, true) = Class.init class; |
135 |
134 |
136 fun gen_init before_exit target thy = |
135 fun init before_exit target thy = |
137 let |
136 let |
138 val name_data = make_name_data thy target; |
137 val name_data = make_name_data thy target; |
139 val background_naming = |
138 val background_naming = |
140 Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name target); |
139 Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name target); |
141 in |
140 in |
153 pretty = pretty name_data, |
152 pretty = pretty name_data, |
154 exit = the_default I before_exit |
153 exit = the_default I before_exit |
155 #> Local_Theory.target_of #> Sign.change_end_local} |
154 #> Local_Theory.target_of #> Sign.change_end_local} |
156 end; |
155 end; |
157 |
156 |
158 val init = gen_init NONE |
157 val theory_init = init NONE ""; |
159 |
|
160 val theory_init = init ""; |
|
161 |
|
162 fun theory_map f = theory_init #> f #> Local_Theory.exit_global; |
158 fun theory_map f = theory_init #> f #> Local_Theory.exit_global; |
163 |
|
164 fun theory_like_init before_exit = gen_init (SOME before_exit) ""; |
|
165 |
159 |
166 |
160 |
167 (* toplevel interaction *) |
161 (* toplevel interaction *) |
168 |
162 |
169 fun begin ("-", _) thy = theory_init thy |
163 fun begin ("-", _) thy = theory_init thy |
170 | begin target thy = init (Locale.check thy target) thy; |
164 | begin target thy = init NONE (Locale.check thy target) thy; |
171 |
165 |
172 val exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global; |
166 val exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global; |
173 |
167 |
174 fun switch NONE (Context.Theory thy) = |
168 fun switch NONE (Context.Theory thy) = |
175 (Context.Theory o exit, theory_init thy) |
169 (Context.Theory o exit, theory_init thy) |
176 | switch (SOME name) (Context.Theory thy) = |
170 | switch (SOME name) (Context.Theory thy) = |
177 (Context.Theory o exit, begin name thy) |
171 (Context.Theory o exit, begin name thy) |
178 | switch NONE (Context.Proof lthy) = |
172 | switch NONE (Context.Proof lthy) = |
179 (Context.Proof o Local_Theory.reset, lthy) |
173 (Context.Proof o Local_Theory.reset, lthy) |
180 | switch (SOME name) (Context.Proof lthy) = |
174 | switch (SOME name) (Context.Proof lthy) = |
181 (Context.Proof o init (target_of lthy) o exit, |
175 (Context.Proof o init NONE (target_of lthy) o exit, |
182 (begin name o exit o Local_Theory.assert_nonbrittle) lthy); |
176 (begin name o exit o Local_Theory.assert_nonbrittle) lthy); |
183 |
177 |
184 end; |
178 end; |