91 let val decls = maps (the_bundle ctxt o prep ctxt) args |
91 let val decls = maps (the_bundle ctxt o prep ctxt) args |
92 in #2 (Attrib.local_notes "" [((Binding.empty, []), decls)] ctxt) end; |
92 in #2 (Attrib.local_notes "" [((Binding.empty, []), decls)] ctxt) end; |
93 |
93 |
94 fun gen_context prep_bundle prep_decl raw_incls raw_elems gthy = |
94 fun gen_context prep_bundle prep_decl raw_incls raw_elems gthy = |
95 let |
95 let |
96 val lthy = Context.cases Named_Target.theory_init Local_Theory.assert gthy; |
96 val (after_close, lthy) = |
97 fun augment ctxt = |
97 gthy |> Context.cases (pair Local_Theory.exit o Named_Target.theory_init) |
98 let |
98 (pair I o Local_Theory.assert); |
99 val ((_, _, _, ctxt'), _) = ctxt |
99 val ((_, _, _, lthy'), _) = lthy |
100 |> Context_Position.restore_visible lthy |
100 |> gen_includes prep_bundle raw_incls |
101 |> gen_includes prep_bundle raw_incls |
101 |> prep_decl ([], []) I raw_elems; |
102 |> prep_decl ([], []) I raw_elems; |
|
103 in ctxt' |> Context_Position.restore_visible ctxt end; |
|
104 in |
102 in |
105 (case gthy of |
103 lthy' |> Local_Theory.open_target |
106 Context.Theory _ => Local_Theory.target augment lthy |> Local_Theory.restore |
104 (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy) after_close |
107 | Context.Proof _ => |
|
108 augment lthy |> |
|
109 Local_Theory.open_target (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy)) |
|
110 end; |
105 end; |
111 |
106 |
112 in |
107 in |
113 |
108 |
114 val includes = gen_includes (K I); |
109 val includes = gen_includes (K I); |