src/Pure/Isar/named_target.ML

--- 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