src/Pure/Isar/theory_target.ML

 Common theory targets.
 *)
 
 signature THEORY_TARGET =
 sig
+  val peek: local_theory -> string option
   val begin: bstring -> Proof.context -> local_theory
   val init: xstring option -> theory -> local_theory
   val init_i: string option -> theory -> local_theory
   val mapping: xstring option -> (local_theory -> local_theory) -> theory -> Proof.context * theory
 end;
 
 structure TheoryTarget: THEORY_TARGET =
 struct
 
 (** locale targets **)
+
+(* context data *)
+
+structure Data = ProofDataFun
+(
+  val name = "Isar/theory_target";
+  type T = string option;
+  fun init _ = NONE;
+  fun print _ _ = ();
+);
+
+val _ = Context.add_setup Data.init;
+val peek = Data.get;
+
 
 (* pretty *)
 
 fun pretty loc ctxt =
   let

     axioms = axioms,
     defs = defs,
     notes = notes loc,
     term_syntax = term_syntax loc,
     declaration = declaration loc,
-    exit = K I};
+    exit = K I}
+  #> Data.put (SOME loc);
 
 fun init_i NONE thy = begin "" (ProofContext.init thy)
   | init_i (SOME loc) thy = begin loc (Locale.init loc thy);
 
 fun init loc thy = init_i (Option.map (Locale.intern thy) loc) thy;