1.1 --- a/src/Pure/Isar/theory_target.ML	Mon Nov 05 20:50:43 2007 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Nov 05 20:50:44 2007 +0100
     1.3 @@ -9,8 +9,8 @@
     1.4  sig
     1.5    val peek: local_theory -> {target: string, is_locale: bool, is_class: bool}
     1.6    val init: string option -> theory -> local_theory
     1.7 -  val init_cmd: xstring -> theory -> local_theory
     1.8    val begin: string -> Proof.context -> local_theory
     1.9 +  val context: xstring -> theory -> local_theory
    1.10  end;
    1.11  
    1.12  structure TheoryTarget: THEORY_TARGET =
    1.13 @@ -20,15 +20,15 @@
    1.14  
    1.15  datatype target = Target of {target: string, is_locale: bool, is_class: bool};
    1.16  
    1.17 -fun make_target thy NONE =
    1.18 -      Target {target = "", is_locale = false, is_class = false}
    1.19 -  | make_target thy (SOME target) =
    1.20 -      Target {target = target, is_locale = true, is_class = Class.is_class thy target};
    1.21 +fun make_target target is_locale is_class =
    1.22 +  Target {target = target, is_locale = is_locale, is_class = is_class};
    1.23 +
    1.24 +val global_target = make_target "" false false;
    1.25  
    1.26  structure Data = ProofDataFun
    1.27  (
    1.28    type T = target;
    1.29 -  fun init thy = make_target thy NONE;
    1.30 +  fun init _ = global_target;
    1.31  );
    1.32  
    1.33  val peek = (fn Target args => args) o Data.get;
    1.34 @@ -297,56 +297,42 @@
    1.35    end;
    1.36  
    1.37  
    1.38 -(* init and exit *)
    1.39 +(* init *)
    1.40 +
    1.41 +local
    1.42  
    1.43 -fun init_ctxt ta thy =
    1.44 -  let
    1.45 -    val Target {target = target, is_locale = is_locale, is_class = is_class} = ta
    1.46 -  in
    1.47 -    thy
    1.48 -    |> (if is_locale then Locale.init target else ProofContext.init)
    1.49 -    |> is_class ? Class.init target
    1.50 -  end;
    1.51 +fun init_target _ NONE = global_target
    1.52 +  | init_target thy (SOME target) = make_target target true (Class.is_class thy target);
    1.53 +
    1.54 +fun init_ctxt (Target {target, is_locale, is_class}) =
    1.55 +  (if is_locale then Locale.init target else ProofContext.init) #>
    1.56 +  is_class ? Class.init target;
    1.57  
    1.58 -fun init_ops ta init_ctxt =
    1.59 -  let
    1.60 -    val Target {target = target, ...} = ta;
    1.61 -  in
    1.62 -    Data.put ta
    1.63 -    #> LocalTheory.init (NameSpace.base target)
    1.64 -     {pretty = pretty ta,
    1.65 -      axioms = axioms ta,
    1.66 -      abbrev = abbrev ta,
    1.67 -      define = define ta,
    1.68 -      notes = notes ta,
    1.69 -      type_syntax = type_syntax ta,
    1.70 -      term_syntax = term_syntax ta,
    1.71 -      declaration = declaration ta,
    1.72 -      target_naming = target_naming ta,
    1.73 -      reinit = fn _ => init_ops ta init_ctxt o init_ctxt,
    1.74 -      exit = LocalTheory.target_of}
    1.75 -  end;
    1.76 +fun init_lthy (ta as Target {target, ...}) =
    1.77 +  Data.put ta #>
    1.78 +  LocalTheory.init (NameSpace.base target)
    1.79 +   {pretty = pretty ta,
    1.80 +    axioms = axioms ta,
    1.81 +    abbrev = abbrev ta,
    1.82 +    define = define ta,
    1.83 +    notes = notes ta,
    1.84 +    type_syntax = type_syntax ta,
    1.85 +    term_syntax = term_syntax ta,
    1.86 +    declaration = declaration ta,
    1.87 +    target_naming = target_naming ta,
    1.88 +    reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy),
    1.89 +    exit = LocalTheory.target_of}
    1.90 +and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta;
    1.91  
    1.92 -fun init target thy =
    1.93 -  let
    1.94 -    val ta = make_target thy target;
    1.95 -    val init_ctxt = init_ctxt ta;
    1.96 -  in
    1.97 -    thy
    1.98 -    |> init_ctxt
    1.99 -    |> init_ops ta init_ctxt
   1.100 -  end;
   1.101 +in
   1.102  
   1.103 -fun begin target ctxt =
   1.104 -  let
   1.105 -    val thy = ProofContext.theory_of ctxt;
   1.106 -    val ta = make_target thy (SOME target);
   1.107 -  in
   1.108 -    ctxt
   1.109 -    |> init_ops ta (init_ctxt ta)
   1.110 -  end;
   1.111 +fun init target thy = init_lthy_ctxt (init_target thy target) thy;
   1.112 +fun begin target ctxt = init_lthy (init_target (ProofContext.theory_of ctxt) (SOME target)) ctxt;
   1.113  
   1.114 -fun init_cmd "-" thy = init NONE thy
   1.115 -  | init_cmd target thy = init (SOME (Locale.intern thy target)) thy;
   1.116 +fun context "-" thy = init NONE thy
   1.117 +  | context target thy = init (SOME (Locale.intern thy target)) thy;
   1.118  
   1.119  end;
   1.120 +
   1.121 +end;
   1.122 +