clarified theory target interface

--- a/src/Pure/Isar/isar_syn.ML	Fri Nov 02 18:52:59 2007 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Nov 02 18:53:00 2007 +0100
@@ -387,7 +387,7 @@
 val _ =
   OuterSyntax.command "context" "enter local theory context" K.thy_decl
     (P.name --| P.begin >> (fn name =>
-      Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.init_cmd (SOME name))));
+      Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.init_cmd name)));
 
 
 (* locales *)

--- a/src/Pure/Isar/theory_target.ML	Fri Nov 02 18:52:59 2007 +0100
+++ b/src/Pure/Isar/theory_target.ML	Fri Nov 02 18:53:00 2007 +0100
@@ -8,9 +8,9 @@
 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 =
@@ -20,13 +20,15 @@
 
 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;
@@ -297,17 +299,21 @@
 
 (* init and exit *)
 
-fun begin target ctxt =
+fun init_ctxt ta thy =
   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};
+    val Target {target = target, is_locale = is_locale, is_class = is_class} = ta
   in
-    ctxt
-    |> Data.put ta
+    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,
@@ -317,15 +323,30 @@
       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 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 init_cmd (SOME "-") thy = init NONE thy
-  | init_cmd target thy = init (Option.map (Locale.intern thy) target) thy;
+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;

--- a/src/Pure/Isar/toplevel.ML	Fri Nov 02 18:52:59 2007 +0100
+++ b/src/Pure/Isar/toplevel.ML	Fri Nov 02 18:53:00 2007 +0100
@@ -118,9 +118,10 @@
 
 val loc_exit = ProofContext.theory_of o LocalTheory.exit;
 
-fun loc_begin loc (Context.Theory thy) = loc_init loc thy
+fun loc_begin NONE (Context.Theory thy) = loc_init "-" thy
+  | loc_begin (SOME loc) (Context.Theory thy) = loc_init loc thy
   | loc_begin NONE (Context.Proof lthy) = lthy
-  | loc_begin loc (Context.Proof lthy) = loc_init loc (loc_exit lthy);
+  | loc_begin (SOME loc) (Context.Proof lthy) = loc_init loc (loc_exit lthy);
 
 fun loc_finish _ (Context.Theory _) = Context.Theory o loc_exit
   | loc_finish NONE (Context.Proof _) = Context.Proof o LocalTheory.restore
@@ -147,7 +148,7 @@
 fun presentation_context (SOME (Theory (_, SOME ctxt))) NONE = ctxt
   | presentation_context (SOME node) NONE = cases_node Context.proof_of Proof.context_of node
   | presentation_context (SOME node) (SOME loc) =
-      loc_init (SOME loc) (cases_node Context.theory_of Proof.theory_of node)
+      loc_init loc (cases_node Context.theory_of Proof.theory_of node)
   | presentation_context NONE _ = raise UNDEF;
 
 
@@ -207,7 +208,7 @@
 
 (* print state *)
 
-val pretty_context = LocalTheory.pretty o Context.cases (loc_init NONE) I;
+val pretty_context = LocalTheory.pretty o Context.cases (loc_init "-") I;
 
 fun print_state_context state =
   (case try node_of state of