--- a/src/Pure/Isar/bundle.ML Fri Aug 04 08:12:57 2017 +0200
+++ b/src/Pure/Isar/bundle.ML Fri Aug 04 08:12:58 2017 +0200
@@ -175,12 +175,10 @@
fun init binding thy =
thy
- |> Sign.change_begin
- |> set_target []
- |> Proof_Context.init_global
- |> Local_Theory.init
+ |> Generic_Target.init
{background_naming = Sign.naming_of thy,
- exit = conclude false binding #> #2 #> Local_Theory.target_of #> Sign.change_end_local}
+ setup = set_target [] #> Proof_Context.init_global,
+ conclude = conclude false binding #> #2}
{define = bad_operation,
notes = bundle_notes,
abbrev = bad_operation,
--- a/src/Pure/Isar/class.ML Fri Aug 04 08:12:57 2017 +0200
+++ b/src/Pure/Isar/class.ML Fri Aug 04 08:12:58 2017 +0200
@@ -683,20 +683,19 @@
| NONE => NONE);
in
thy
- |> Sign.change_begin
- |> Proof_Context.init_global
- |> Instantiation.put (make_instantiation ((tycos, vs, sort), params))
- |> fold (Variable.declare_typ o TFree) vs
- |> fold (Variable.declare_names o Free o snd) params
- |> (Overloading.map_improvable_syntax) (K {primary_constraints = primary_constraints,
- secondary_constraints = [], improve = improve, subst = K NONE,
- no_subst_in_abbrev_mode = false, unchecks = []})
- |> Overloading.activate_improvable_syntax
- |> Context.proof_map (Syntax_Phases.term_check 0 "resorting" resort_check)
- |> synchronize_inst_syntax
- |> Local_Theory.init
+ |> Generic_Target.init
{background_naming = Sign.naming_of thy,
- exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
+ setup = Proof_Context.init_global
+ #> Instantiation.put (make_instantiation ((tycos, vs, sort), params))
+ #> fold (Variable.declare_typ o TFree) vs
+ #> fold (Variable.declare_names o Free o snd) params
+ #> (Overloading.map_improvable_syntax) (K {primary_constraints = primary_constraints,
+ secondary_constraints = [], improve = improve, subst = K NONE,
+ no_subst_in_abbrev_mode = false, unchecks = []})
+ #> Overloading.activate_improvable_syntax
+ #> Context.proof_map (Syntax_Phases.term_check 0 "resorting" resort_check)
+ #> synchronize_inst_syntax,
+ conclude = conclude}
{define = Generic_Target.define foundation,
notes = Generic_Target.notes Generic_Target.theory_target_notes,
abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev,
--- a/src/Pure/Isar/generic_target.ML Fri Aug 04 08:12:57 2017 +0200
+++ b/src/Pure/Isar/generic_target.ML Fri Aug 04 08:12:58 2017 +0200
@@ -76,6 +76,11 @@
local_theory -> local_theory
val locale_dependency: string -> string * morphism -> (morphism * bool) option -> morphism ->
local_theory -> local_theory
+
+ (*initialisation*)
+ val init: {background_naming: Name_Space.naming, setup: theory -> Proof.context,
+ conclude: local_theory -> local_theory} ->
+ Local_Theory.operations -> theory -> local_theory
end
structure Generic_Target: GENERIC_TARGET =
@@ -417,4 +422,16 @@
fun locale_abbrev locale = abbrev (locale_target_abbrev locale);
+
+(** initialisation **)
+
+fun init {background_naming, setup, conclude} operations thy =
+ thy
+ |> Sign.change_begin
+ |> setup
+ |> Local_Theory.init
+ {background_naming = background_naming,
+ exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
+ operations;
+
end;
--- a/src/Pure/Isar/named_target.ML Fri Aug 04 08:12:57 2017 +0200
+++ b/src/Pure/Isar/named_target.ML Fri Aug 04 08:12:58 2017 +0200
@@ -130,12 +130,10 @@
val target = make_target thy ident;
in
thy
- |> Sign.change_begin
- |> init_context target
- |> setup
- |> Local_Theory.init
+ |> Generic_Target.init
{background_naming = Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name ident),
- exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
+ setup = init_context target #> setup,
+ conclude = conclude}
{define = Generic_Target.define (foundation target),
notes = Generic_Target.notes (notes target),
abbrev = abbrev target,
--- a/src/Pure/Isar/overloading.ML Fri Aug 04 08:12:57 2017 +0200
+++ b/src/Pure/Isar/overloading.ML Fri Aug 04 08:12:58 2017 +0200
@@ -193,15 +193,14 @@
(Term.dest_Const (prep_const ctxt const), (v, checked)));
in
thy
- |> Sign.change_begin
- |> Proof_Context.init_global
- |> Data.put overloading
- |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
- |> activate_improvable_syntax
- |> synchronize_syntax
- |> Local_Theory.init
+ |> Generic_Target.init
{background_naming = Sign.naming_of thy,
- exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
+ setup = Proof_Context.init_global
+ #> Data.put overloading
+ #> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
+ #> activate_improvable_syntax
+ #> synchronize_syntax,
+ conclude = conclude}
{define = Generic_Target.define foundation,
notes = Generic_Target.notes Generic_Target.theory_target_notes,
abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev,