# HG changeset patch
# User haftmann
# Date 1501827178 -7200
# Node ID 5caea089dd17013e6805f973aac7f4a5125b2e78
# Parent  13e7dc5f7c3d761291c12d55effa16298393ec40
more structural sharing between common target Generic_Target.init

diff -r 13e7dc5f7c3d -r 5caea089dd17 src/Pure/Isar/bundle.ML
--- 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,
diff -r 13e7dc5f7c3d -r 5caea089dd17 src/Pure/Isar/class.ML
--- 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,
diff -r 13e7dc5f7c3d -r 5caea089dd17 src/Pure/Isar/generic_target.ML
--- 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;
diff -r 13e7dc5f7c3d -r 5caea089dd17 src/Pure/Isar/named_target.ML
--- 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,
diff -r 13e7dc5f7c3d -r 5caea089dd17 src/Pure/Isar/overloading.ML
--- 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,