equal
deleted
inserted
replaced
303 |
303 |
304 fun init_target _ NONE = global_target |
304 fun init_target _ NONE = global_target |
305 | init_target thy (SOME target) = make_target target true (Class.is_class thy target); |
305 | init_target thy (SOME target) = make_target target true (Class.is_class thy target); |
306 |
306 |
307 fun init_ctxt (Target {target, is_locale, is_class}) = |
307 fun init_ctxt (Target {target, is_locale, is_class}) = |
308 if is_locale then if is_class then Class.init target |
308 if not is_locale then ProofContext.init |
309 else Locale.init target else ProofContext.init; |
309 else if not is_class then Locale.init target |
|
310 else Class.init target; |
310 |
311 |
311 fun init_lthy (ta as Target {target, ...}) = |
312 fun init_lthy (ta as Target {target, ...}) = |
312 Data.put ta #> |
313 Data.put ta #> |
313 LocalTheory.init (NameSpace.base target) |
314 LocalTheory.init (NameSpace.base target) |
314 {pretty = pretty ta, |
315 {pretty = pretty ta, |