support for bundle definition via target;

--- a/src/Pure/Isar/bundle.ML	Thu Jun 09 12:21:15 2016 +0200
+++ b/src/Pure/Isar/bundle.ML	Thu Jun 09 15:41:49 2016 +0200
@@ -9,10 +9,12 @@
   val check: Proof.context -> xstring * Position.T -> string
   val get_bundle: Proof.context -> string -> Attrib.thms
   val get_bundle_cmd: Proof.context -> xstring * Position.T -> Attrib.thms
+  val print_bundles: bool -> Proof.context -> unit
   val bundle: binding * Attrib.thms ->
     (binding * typ option * mixfix) list -> local_theory -> local_theory
   val bundle_cmd: binding * (Facts.ref * Token.src list) list ->
     (binding * string option * mixfix) list -> local_theory -> local_theory
+  val init: binding -> theory -> local_theory
   val includes: string list -> Proof.context -> Proof.context
   val includes_cmd: (xstring * Position.T) list -> Proof.context -> Proof.context
   val include_: string list -> Proof.state -> Proof.state
@@ -23,34 +25,82 @@
     generic_theory -> Binding.scope * local_theory
   val context_cmd: (xstring * Position.T) list -> Element.context list ->
     generic_theory -> Binding.scope * local_theory
-  val print_bundles: bool -> Proof.context -> unit
 end;
 
 structure Bundle: BUNDLE =
 struct
 
-(* maintain bundles *)
+(** context data **)
+
+structure Data = Generic_Data
+(
+  type T = Attrib.thms Name_Space.table * Attrib.thms option;
+  val empty : T = (Name_Space.empty_table "bundle", NONE);
+  val extend = I;
+  fun merge ((tab1, target1), (tab2, target2)) =
+    (Name_Space.merge_tables (tab1, tab2), merge_options (target1, target2));
+);
+
+
+(* bundles *)
+
+val get_bundles_generic = #1 o Data.get;
+val get_bundles = get_bundles_generic o Context.Proof;
+
+fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_bundles ctxt);
+
+val get_bundle_generic = Name_Space.get o get_bundles_generic;
+val get_bundle = get_bundle_generic o Context.Proof;
+fun get_bundle_cmd ctxt = get_bundle ctxt o check ctxt;
+
+fun define_bundle def context =
+  let
+    val (name, bundles') = Name_Space.define context true def (get_bundles_generic context);
+    val context' = (Data.map o apfst o K) bundles' context;
+  in (name, context') end;
+
+
+(* target -- bundle under construction *)
+
+fun the_target thy =
+  (case #2 (Data.get (Context.Theory thy)) of
+    SOME thms => thms
+  | NONE => error "Missing bundle target");
+
+val reset_target = (Context.theory_map o Data.map o apsnd o K) NONE;
+val set_target = Context.theory_map o Data.map o apsnd o K o SOME;
+
+fun augment_target thms =
+  Local_Theory.background_theory (fn thy => set_target (the_target thy @ thms) thy);
+
+
+(* print bundles *)
+
+fun pretty_bundle ctxt (markup_name, bundle) =
+  let
+    val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt;
+
+    fun prt_thms (ths, []) = map prt_thm ths
+      | prt_thms (ths, atts) = Pretty.enclose "(" ")"
+          (Pretty.breaks (map prt_thm ths)) :: Attrib.pretty_attribs ctxt atts;
+  in
+    Pretty.block ([Pretty.keyword1 "bundle", Pretty.str " ", Pretty.mark_str markup_name] @
+      (if null bundle then [] else Pretty.breaks (Pretty.str " =" :: maps prt_thms bundle)))
+  end;
+
+fun print_bundles verbose ctxt =
+  Pretty.writeln_chunks
+    (map (pretty_bundle ctxt) (Name_Space.markup_table verbose ctxt (get_bundles ctxt)));
+
+
+
+(** define bundle **)
 
 fun transform_bundle phi =
   map (fn (fact, atts) => (Morphism.fact phi fact, (map o map) (Token.transform phi) atts));
 
-structure Data = Generic_Data
-(
-  type T = Attrib.thms Name_Space.table;
-  val empty : T = Name_Space.empty_table "bundle";
-  val extend = I;
-  val merge = Name_Space.merge_tables;
-);
 
-val get_bundles = Data.get o Context.Proof;
-
-fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_bundles ctxt);
-
-val get_bundle = Name_Space.get o get_bundles;
-fun get_bundle_cmd ctxt = get_bundle ctxt o check ctxt;
-
-
-(* define bundle *)
+(* command *)
 
 local
 
@@ -64,10 +114,7 @@
       |> transform_bundle (Proof_Context.export_morphism ctxt' lthy);
   in
     lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
-      (fn phi => fn context =>
-        context |> Data.map
-          (#2 o Name_Space.define context true
-            (Morphism.binding phi binding, transform_bundle phi bundle)))
+      (fn phi => #2 o define_bundle (Morphism.binding phi binding, transform_bundle phi bundle))
   end;
 
 in
@@ -78,7 +125,67 @@
 end;
 
 
-(* include bundles *)
+(* target *)
+
+local
+
+fun bad_operation _ = error "Not possible in bundle target";
+
+fun conclude binding =
+  Local_Theory.background_theory_result (fn thy =>
+    let
+      val (name, Context.Theory thy') =
+        define_bundle (binding, the_target thy) (Context.Theory thy);
+    in (name, reset_target thy') end);
+
+fun pretty binding lthy =
+  let
+    val bundle = the_target (Proof_Context.theory_of lthy);
+    val (name, lthy') = conclude binding lthy;
+    val thy_ctxt' = Proof_Context.init_global (Proof_Context.theory_of lthy');
+    val markup_name =
+      Name_Space.markup_extern thy_ctxt' (Name_Space.space_of_table (get_bundles thy_ctxt')) name;
+  in [pretty_bundle lthy' (markup_name, bundle)] end;
+
+fun bundle_notes kind facts lthy =
+  let
+    val bundle = facts
+      |> maps (fn ((_, more_atts), thms) => map (fn (ths, atts) => (ths, atts @ more_atts)) thms);
+  in
+    lthy
+    |> augment_target (transform_bundle (Local_Theory.standard_morphism_theory lthy) bundle)
+    |> Generic_Target.standard_notes (K true) kind facts
+    |> Attrib.local_notes kind facts
+  end;
+
+fun bundle_declaration decl lthy =
+  lthy
+  |> (augment_target o Attrib.internal_declaration)
+    (Morphism.transform (Local_Theory.standard_morphism_theory lthy) decl)
+  |> Generic_Target.standard_declaration (K true) decl;
+
+in
+
+fun init binding thy =
+  thy
+  |> Sign.change_begin
+  |> set_target []
+  |> Proof_Context.init_global
+  |> Local_Theory.init (Sign.naming_of thy)
+     {define = bad_operation,
+      notes = bundle_notes,
+      abbrev = bad_operation,
+      declaration = K bundle_declaration,
+      theory_registration = bad_operation,
+      locale_dependency = bad_operation,
+      pretty = pretty binding,
+      exit = conclude binding #> #2 #> Local_Theory.target_of #> Sign.change_end_local}
+
+end;
+
+
+
+(** include bundles **)
 
 local
 
@@ -120,22 +227,4 @@
 
 end;
 
-
-(* print_bundles *)
-
-fun print_bundles verbose ctxt =
-  let
-    val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt;
-
-    fun prt_fact (ths, []) = map prt_thm ths
-      | prt_fact (ths, atts) = Pretty.enclose "(" ")"
-          (Pretty.breaks (map prt_thm ths)) :: Attrib.pretty_attribs ctxt atts;
-
-    fun prt_bundle (name, bundle) =
-      Pretty.block (Pretty.keyword1 "bundle" :: Pretty.str " " :: Pretty.mark_str name ::
-        Pretty.breaks (Pretty.str " =" :: maps prt_fact bundle));
-  in
-    map prt_bundle (Name_Space.markup_table verbose ctxt (get_bundles ctxt))
-  end |> Pretty.writeln_chunks;
-
 end;

--- a/src/Pure/Isar/local_theory.ML	Thu Jun 09 12:21:15 2016 +0200
+++ b/src/Pure/Isar/local_theory.ML	Thu Jun 09 15:41:49 2016 +0200
@@ -31,6 +31,7 @@
   val new_group: local_theory -> local_theory
   val reset_group: local_theory -> local_theory
   val standard_morphism: local_theory -> Proof.context -> morphism
+  val standard_morphism_theory: local_theory -> morphism
   val standard_form: local_theory -> Proof.context -> (morphism -> 'a) -> 'a
   val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   val raw_theory: (theory -> theory) -> local_theory -> local_theory
@@ -195,6 +196,9 @@
   Morphism.binding_morphism "Local_Theory.standard_binding"
     (Name_Space.transform_binding (Proof_Context.naming_of lthy));
 
+fun standard_morphism_theory lthy =
+  standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
+
 fun standard_form lthy ctxt x =
   Morphism.form (Morphism.transform (standard_morphism lthy ctxt) x);
 

--- a/src/Pure/Pure.thy	Thu Jun 09 12:21:15 2016 +0200
+++ b/src/Pure/Pure.thy	Thu Jun 09 15:41:49 2016 +0200
@@ -32,6 +32,7 @@
     "parse_ast_translation" "parse_translation" "print_translation"
     "typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML"
   and "bundle" :: thy_decl
+  and "bundle_target" :: thy_decl_block
   and "include" "including" :: prf_decl
   and "print_bundles" :: diag
   and "context" "locale" "experiment" :: thy_decl_block
@@ -496,6 +497,10 @@
       >> (uncurry Bundle.bundle_cmd));
 
 val _ =
+  Outer_Syntax.command @{command_keyword bundle_target} "define bundle of declarations"
+    (Parse.binding --| Parse.begin >> (Toplevel.begin_local_theory true o Bundle.init));
+
+val _ =
   Outer_Syntax.command @{command_keyword include}
     "include declarations from bundle in proof body"
     (Scan.repeat1 (Parse.position Parse.name) >> (Toplevel.proof o Bundle.include_cmd));