named target is optional; explicit Name_Target.reinit

--- a/src/Pure/Isar/named_target.ML	Thu Aug 12 13:42:12 2010 +0200
+++ b/src/Pure/Isar/named_target.ML	Thu Aug 12 13:42:13 2010 +0200
@@ -7,10 +7,11 @@
 
 signature NAMED_TARGET =
 sig
-  val peek: local_theory -> {target: string, is_locale: bool, is_class: bool}
   val init: string -> theory -> local_theory
   val theory_init: theory -> local_theory
+  val reinit: local_theory -> local_theory -> local_theory
   val context_cmd: xstring -> theory -> local_theory
+  val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option
 end;
 
 structure Named_Target: NAMED_TARGET =
@@ -33,11 +34,11 @@
 
 structure Data = Proof_Data
 (
-  type T = target;
-  fun init _ = global_target;
+  type T = target option;
+  fun init _ = NONE;
 );
 
-val peek = (fn Target args => args) o Data.get;
+val peek = Option.map (fn Target args => args) o Data.get;
 
 
 (* generic declarations *)
@@ -187,7 +188,7 @@
 fun init_target (ta as Target {target, ...}) thy =
   thy
   |> init_context ta
-  |> Data.put ta
+  |> Data.put (SOME ta)
   |> Local_Theory.init NONE (Long_Name.base_name target)
      {define = Generic_Target.define (target_foundation ta),
       notes = Generic_Target.notes (target_notes ta),
@@ -203,6 +204,10 @@
 
 fun init target thy = init_target (named_target thy target) thy;
 
+fun reinit lthy = case peek lthy
+ of SOME {target, ...} => init target o Local_Theory.exit_global
+  | NONE => error "Not in a named target";
+
 val theory_init = init_target global_target;
 
 fun context_cmd "-" thy = init "" thy

--- a/src/Pure/Isar/toplevel.ML	Thu Aug 12 13:42:12 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Thu Aug 12 13:42:13 2010 +0200
@@ -107,13 +107,11 @@
 
 fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy
   | loc_begin NONE (Context.Proof lthy) = lthy
-  | loc_begin (SOME loc) (Context.Proof lthy) = loc_init loc (loc_exit lthy);
+  | loc_begin (SOME loc) (Context.Proof lthy) = (loc_init loc o loc_exit) lthy;
 
 fun loc_finish _ (Context.Theory _) = Context.Theory o loc_exit
   | loc_finish NONE (Context.Proof _) = Context.Proof o Local_Theory.restore
-  | loc_finish (SOME _) (Context.Proof lthy) = fn lthy' => let
-        val target = #target (Named_Target.peek lthy);
-      in Context.Proof (Named_Target.init target (loc_exit lthy')) end;
+  | loc_finish (SOME _) (Context.Proof lthy) = Context.Proof o Named_Target.reinit lthy;
 
 
 (* datatype node *)