src/Pure/Isar/theory_target.ML

 *)
 
 signature THEORY_TARGET =
 sig
   val peek: local_theory -> {target: string, is_locale: bool, is_class: bool}
+  val init: string option -> theory -> local_theory
+  val init_cmd: xstring -> theory -> local_theory
   val begin: string -> Proof.context -> local_theory
-  val init: string option -> theory -> local_theory
-  val init_cmd: xstring option -> theory -> local_theory
 end;
 
 structure TheoryTarget: THEORY_TARGET =
 struct
 
 (* context data *)
 
 datatype target = Target of {target: string, is_locale: bool, is_class: bool};
 
-fun make_target target is_locale is_class =
-  Target {target = target, is_locale = is_locale, is_class = is_class};
+fun make_target thy NONE =
+      Target {target = "", is_locale = false, is_class = false}
+  | make_target thy (SOME target) =
+      Target {target = target, is_locale = true, is_class = Class.is_class thy target};
 
 structure Data = ProofDataFun
 (
   type T = target;
-  fun init _ = make_target "" false false;
+  fun init thy = make_target thy NONE;
 );
 
 val peek = (fn Target args => args) o Data.get;
 
 

   end;
 
 
 (* init and exit *)
 
-fun begin target ctxt =
-  let
-    val thy = ProofContext.theory_of ctxt;
-    val is_locale = target <> "";
-    val is_class = Class.is_class thy target;
-    val ta = Target {target = target, is_locale = is_locale, is_class = is_class};
-  in
-    ctxt
-    |> Data.put ta
+fun init_ctxt ta thy =
+  let
+    val Target {target = target, is_locale = is_locale, is_class = is_class} = ta
+  in
+    thy
+    |> (if is_locale then Locale.init target else ProofContext.init)
     |> is_class ? Class.init target
-    |> LocalTheory.init (NameSpace.base target)
+  end;
+
+fun init_ops ta init_ctxt =
+  let
+    val Target {target = target, ...} = ta;
+  in
+    Data.put ta
+    #> LocalTheory.init (NameSpace.base target)
      {pretty = pretty ta,
       axioms = axioms ta,
       abbrev = abbrev ta,
       define = define ta,
       notes = notes ta,
       type_syntax = type_syntax ta,
       term_syntax = term_syntax ta,
       declaration = declaration ta,
       target_naming = target_naming ta,
-      reinit = fn _ =>
-        begin target o (if is_locale then Locale.init target else ProofContext.init),
+      reinit = fn _ => init_ops ta init_ctxt o init_ctxt,
       exit = LocalTheory.target_of}
   end;
 
-fun init NONE thy = begin "" (ProofContext.init thy)
-  | init (SOME target) thy = begin target (Locale.init target thy);
-
-fun init_cmd (SOME "-") thy = init NONE thy
-  | init_cmd target thy = init (Option.map (Locale.intern thy) target) thy;
+fun init target thy =
+  let
+    val ta = make_target thy target;
+    val init_ctxt = init_ctxt ta;
+  in
+    thy
+    |> init_ctxt
+    |> init_ops ta init_ctxt
+  end;
+
+fun begin target ctxt =
+  let
+    val thy = ProofContext.theory_of ctxt;
+    val ta = make_target thy (SOME target);
+  in
+    ctxt
+    |> init_ops ta (init_ctxt ta)
+  end;
+
+fun init_cmd "-" thy = init NONE thy
+  | init_cmd target thy = init (SOME (Locale.intern thy target)) thy;
 
 end;