1.1 --- a/src/Pure/Isar/named_target.ML Wed Jul 02 08:03:49 2014 +0200
1.2 +++ b/src/Pure/Isar/named_target.ML Wed Jul 02 08:03:50 2014 +0200
1.3 @@ -13,6 +13,7 @@
1.4 val class_of: local_theory -> string option
1.5 val init: string -> theory -> local_theory
1.6 val theory_init: theory -> local_theory
1.7 + val theory_like_init: (local_theory -> local_theory) -> theory -> local_theory
1.8 val begin: xstring * Position.T -> theory -> local_theory
1.9 val exit: local_theory -> theory
1.10 val switch: (xstring * Position.T) option -> Context.generic
1.11 @@ -150,7 +151,7 @@
1.12 | init_context (locale, false) = Locale.init locale
1.13 | init_context (class, true) = Class.init class;
1.14
1.15 -fun init target thy =
1.16 +fun gen_init before_exit target thy =
1.17 let
1.18 val name_data = make_name_data thy target;
1.19 val naming = Sign.naming_of thy
1.20 @@ -159,7 +160,7 @@
1.21 thy
1.22 |> Sign.change_begin
1.23 |> init_context name_data
1.24 - |> Data.put (SOME name_data)
1.25 + |> is_none before_exit ? Data.put (SOME name_data)
1.26 |> Local_Theory.init naming
1.27 {define = Generic_Target.define (foundation name_data),
1.28 notes = Generic_Target.notes (notes name_data),
1.29 @@ -167,11 +168,16 @@
1.30 declaration = declaration name_data,
1.31 subscription = subscription name_data,
1.32 pretty = pretty name_data,
1.33 - exit = Local_Theory.target_of #> Sign.change_end_local}
1.34 + exit = the_default I before_exit
1.35 + #> Local_Theory.target_of #> Sign.change_end_local}
1.36 end;
1.37
1.38 +val init = gen_init NONE
1.39 +
1.40 val theory_init = init "";
1.41
1.42 +fun theory_like_init before_exit = gen_init (SOME before_exit) "";
1.43 +
1.44
1.45 (* toplevel interaction *)
1.46