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