src/Pure/Isar/named_target.ML

--- a/src/Pure/Isar/named_target.ML	Sat Jan 15 22:40:17 2011 +0100
+++ b/src/Pure/Isar/named_target.ML	Sun Jan 16 14:57:14 2011 +0100
@@ -7,7 +7,7 @@
 
 signature NAMED_TARGET =
 sig
-  val init: string -> theory -> local_theory
+  val init: (local_theory -> local_theory) -> 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
@@ -19,12 +19,18 @@
 
 (* context data *)
 
-datatype target = Target of {target: string, is_locale: bool, is_class: bool};
+datatype target =
+  Target of {target: string, is_locale: bool, is_class: bool,
+    before_exit: local_theory -> local_theory};
 
-fun named_target _ "" = Target {target = "", is_locale = false, is_class = false}
-  | named_target thy locale =
+fun make_target target is_locale is_class before_exit =
+  Target {target = target, is_locale = is_locale, is_class = is_class,
+    before_exit = before_exit};
+
+fun named_target _ "" before_exit = make_target "" false false before_exit
+  | named_target thy locale before_exit =
       if Locale.defined thy locale
-      then Target {target = locale, is_locale = true, is_class = Class.is_class thy locale}
+      then make_target locale true (Class.is_class thy locale) before_exit
       else error ("No such locale: " ^ quote locale);
 
 structure Data = Proof_Data
@@ -33,7 +39,9 @@
   fun init _ = NONE;
 );
 
-val peek = Option.map (fn Target args => args) o Data.get;
+val peek =
+  Data.get #> Option.map (fn Target {target, is_locale, is_class, ...} =>
+    {target = target, is_locale = is_locale, is_class = is_class});
 
 
 (* generic declarations *)
@@ -169,14 +177,14 @@
 
 (* init *)
 
-fun init_context (Target {target, is_locale, is_class}) =
+fun init_context (Target {target, is_locale, is_class, ...}) =
   if not is_locale then ProofContext.init_global
   else if not is_class then Locale.init target
   else Class.init target;
 
-fun init target thy =
+fun init before_exit target thy =
   let
-    val ta = named_target thy target;
+    val ta = named_target thy target before_exit;
   in
     thy
     |> init_context ta
@@ -190,17 +198,17 @@
         syntax_declaration = fn pervasive => target_declaration ta
           {syntax = true, pervasive = pervasive},
         pretty = pretty ta,
-        exit = Local_Theory.target_of}
+        exit = Local_Theory.target_of o before_exit}
   end;
 
-val theory_init = init "";
+val theory_init = init I "";
 
 fun reinit lthy =
-  (case peek lthy of
-    SOME {target, ...} => init target o Local_Theory.exit_global
+  (case Data.get lthy of
+    SOME (Target {target, before_exit, ...}) => init before_exit target o Local_Theory.exit_global
   | NONE => error "Not in a named target");
 
-fun context_cmd "-" thy = init "" thy
-  | context_cmd target thy = init (Locale.intern thy target) thy;
+fun context_cmd "-" thy = init I "" thy
+  | context_cmd target thy = init I (Locale.intern thy target) thy;
 
 end;