merged
authorpaulson
Fri, 04 Aug 2017 23:07:14 +0200
changeset 66340 91257fbcabee
parent 66338 1a8441ec5ced (diff)
parent 66339 1c5e521a98f1 (current diff)
child 66341 1072edd475dc
merged
--- a/src/Doc/Implementation/Local_Theory.thy	Fri Aug 04 21:30:38 2017 +0200
+++ b/src/Doc/Implementation/Local_Theory.thy	Fri Aug 04 23:07:14 2017 +0200
@@ -91,8 +91,7 @@
 text %mlref \<open>
   \begin{mldecls}
   @{index_ML_type local_theory: Proof.context} \\
-  @{index_ML Named_Target.init: "(local_theory -> local_theory) option ->
-    string -> theory -> local_theory"} \\[1ex]
+  @{index_ML Named_Target.init: "string -> theory -> local_theory"} \\[1ex]
   @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) ->
     local_theory -> (term * (string * thm)) * local_theory"} \\
   @{index_ML Local_Theory.note: "Attrib.binding * thm list ->
--- a/src/HOL/Statespace/state_space.ML	Fri Aug 04 21:30:38 2017 +0200
+++ b/src/HOL/Statespace/state_space.ML	Fri Aug 04 23:07:14 2017 +0200
@@ -298,7 +298,7 @@
 
 fun add_declaration name decl thy =
   thy
-  |> Named_Target.init NONE name
+  |> Named_Target.init name
   |> (fn lthy => Local_Theory.declaration {syntax = false, pervasive = false} (decl lthy) lthy)
   |> Local_Theory.exit_global;
 
--- a/src/Pure/Isar/bundle.ML	Fri Aug 04 21:30:38 2017 +0200
+++ b/src/Pure/Isar/bundle.ML	Fri Aug 04 23:07:14 2017 +0200
@@ -175,18 +175,17 @@
 
 fun init binding thy =
   thy
-  |> Sign.change_begin
-  |> set_target []
-  |> Proof_Context.init_global
-  |> Local_Theory.init (Sign.naming_of thy)
+  |> Generic_Target.init
+     {background_naming = Sign.naming_of thy,
+      setup = set_target [] #> Proof_Context.init_global,
+      conclude = conclude false binding #> #2}
      {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 false binding #> #2 #> Local_Theory.target_of #> Sign.change_end_local}
+      pretty = pretty binding}
 
 end;
 
@@ -216,7 +215,8 @@
       |> prep_decl ([], []) I raw_elems;
   in
     lthy' |> Local_Theory.init_target
-      (Local_Theory.background_naming_of lthy) (Local_Theory.operations_of lthy) after_close
+      {background_naming = Local_Theory.background_naming_of lthy, after_close = after_close}
+      (Local_Theory.operations_of lthy)
   end;
 
 in
--- a/src/Pure/Isar/class.ML	Fri Aug 04 21:30:38 2017 +0200
+++ b/src/Pure/Isar/class.ML	Fri Aug 04 23:07:14 2017 +0200
@@ -683,26 +683,26 @@
       | 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 (Sign.naming_of thy)
+    |> Generic_Target.init
+       {background_naming = Sign.naming_of thy,
+        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,
         declaration = K Generic_Target.theory_declaration,
         theory_registration = Generic_Target.theory_registration,
         locale_dependency = fn _ => error "Not possible in instantiation target",
-        pretty = pretty,
-        exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
+        pretty = pretty}
   end;
 
 fun instantiation_cmd arities thy =
--- a/src/Pure/Isar/class_declaration.ML	Fri Aug 04 21:30:38 2017 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Fri Aug 04 23:07:14 2017 +0200
@@ -327,7 +327,7 @@
     #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class
     #> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class)))
     |> snd
-    |> Named_Target.init NONE class
+    |> Named_Target.init class
     |> pair class
   end;
 
--- a/src/Pure/Isar/code.ML	Fri Aug 04 21:30:38 2017 +0200
+++ b/src/Pure/Isar/code.ML	Fri Aug 04 23:07:14 2017 +0200
@@ -1072,7 +1072,7 @@
       end;
 
 fun pretty_cert _ (Nothing _) =
-      [Pretty.str "(unimplemented)"]
+      []
   | pretty_cert thy (cert as Equations _) =
       (map_filter
         (Option.map (Thm.pretty_thm_global thy o
--- a/src/Pure/Isar/expression.ML	Fri Aug 04 21:30:38 2017 +0200
+++ b/src/Pure/Isar/expression.ML	Fri Aug 04 23:07:14 2017 +0200
@@ -825,7 +825,7 @@
     val loc_ctxt = thy'
       |> Locale.register_locale binding (extraTs, params)
           (asm, rev defs) (a_intro, b_intro) axioms hyp_spec [] (rev notes) (rev deps')
-      |> Named_Target.init NONE name
+      |> Named_Target.init name
       |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
 
   in (name, loc_ctxt) end;
--- a/src/Pure/Isar/generic_target.ML	Fri Aug 04 21:30:38 2017 +0200
+++ b/src/Pure/Isar/generic_target.ML	Fri Aug 04 23:07:14 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/interpretation.ML	Fri Aug 04 21:30:38 2017 +0200
+++ b/src/Pure/Isar/interpretation.ML	Fri Aug 04 23:07:14 2017 +0200
@@ -220,7 +220,7 @@
 fun gen_global_sublocale prep_loc prep_interpretation
     raw_locale expression raw_defs raw_eqns thy =
   let
-    val lthy = Named_Target.init NONE (prep_loc thy raw_locale) thy;
+    val lthy = Named_Target.init (prep_loc thy raw_locale) thy;
     fun setup_proof after_qed =
       Element.witness_proof_eqs
         (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
--- a/src/Pure/Isar/local_theory.ML	Fri Aug 04 21:30:38 2017 +0200
+++ b/src/Pure/Isar/local_theory.ML	Fri Aug 04 23:07:14 2017 +0200
@@ -65,13 +65,14 @@
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val type_alias: binding -> string -> local_theory -> local_theory
   val const_alias: binding -> string -> local_theory -> local_theory
-  val init: Name_Space.naming -> operations -> Proof.context -> local_theory
+  val init: {background_naming: Name_Space.naming, exit: local_theory -> Proof.context} ->
+    operations -> Proof.context -> local_theory
   val exit: local_theory -> Proof.context
   val exit_global: local_theory -> theory
   val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
   val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory
-  val init_target: Name_Space.naming -> operations -> (local_theory -> local_theory) ->
-    local_theory -> Binding.scope * local_theory
+  val init_target: {background_naming: Name_Space.naming, after_close: local_theory -> local_theory} ->
+    operations -> local_theory -> Binding.scope * local_theory
   val open_target: local_theory -> Binding.scope * local_theory
   val close_target: local_theory -> local_theory
 end;
@@ -95,19 +96,19 @@
      local_theory -> local_theory,
   locale_dependency: string * morphism -> (morphism * bool) option -> morphism ->
      local_theory -> local_theory,
-  pretty: local_theory -> Pretty.T list,
-  exit: local_theory -> Proof.context};
+  pretty: local_theory -> Pretty.T list};
 
 type lthy =
  {background_naming: Name_Space.naming,
   operations: operations,
   after_close: local_theory -> local_theory,
+  exit: local_theory -> Proof.context,
   brittle: bool,
   target: Proof.context};
 
-fun make_lthy (background_naming, operations, after_close, brittle, target) : lthy =
+fun make_lthy (background_naming, operations, after_close, exit, brittle, target) : lthy =
   {background_naming = background_naming, operations = operations,
-    after_close = after_close, brittle = brittle, target = target};
+    after_close = after_close, exit = exit, brittle = brittle, target = target};
 
 
 (* context data *)
@@ -146,16 +147,16 @@
 
 fun map_top f =
   assert #>
-  Data.map (fn {background_naming, operations, after_close, brittle, target} :: parents =>
-    make_lthy (f (background_naming, operations, after_close, brittle, target)) :: parents);
+  Data.map (fn {background_naming, operations, after_close, exit, brittle, target} :: parents =>
+    make_lthy (f (background_naming, operations, after_close, exit, brittle, target)) :: parents);
 
 fun reset lthy = #target (top_of lthy) |> Data.put (Data.get lthy);
 
 fun map_contexts f lthy =
   let val n = level lthy in
     lthy |> (Data.map o map_index)
-      (fn (i, {background_naming, operations, after_close, brittle, target}) =>
-        make_lthy (background_naming, operations, after_close, brittle,
+      (fn (i, {background_naming, operations, after_close, exit, brittle, target}) =>
+        make_lthy (background_naming, operations, after_close, exit, brittle,
           target
           |> Context_Position.set_visible false
           |> f (n - i - 1)
@@ -168,8 +169,8 @@
 
 fun mark_brittle lthy =
   if level lthy = 1 then
-    map_top (fn (background_naming, operations, after_close, _, target) =>
-      (background_naming, operations, after_close, true, target)) lthy
+    map_top (fn (background_naming, operations, after_close, exit, _, target) =>
+      (background_naming, operations, after_close, exit, true, target)) lthy
   else lthy;
 
 fun assert_nonbrittle lthy =
@@ -182,8 +183,8 @@
 val background_naming_of = #background_naming o top_of;
 
 fun map_background_naming f =
-  map_top (fn (background_naming, operations, after_close, brittle, target) =>
-    (f background_naming, operations, after_close, brittle, target));
+  map_top (fn (background_naming, operations, after_close, exit, brittle, target) =>
+    (f background_naming, operations, after_close, exit, brittle, target));
 
 val restore_background_naming = map_background_naming o K o background_naming_of;
 
@@ -348,12 +349,14 @@
 
 (* outermost target *)
 
-fun init background_naming operations target =
+fun init {background_naming, exit} operations target =
   target |> Data.map
-    (fn [] => [make_lthy (background_naming, operations, I, false, target)]
+    (fn [] => [make_lthy (background_naming, operations, I, exit, false, target)]
       | _ => error "Local theory already initialized");
 
-val exit = operation #exit;
+val exit_of = #exit o bottom_of;
+
+fun exit lthy = exit_of lthy lthy;
 val exit_global = Proof_Context.theory_of o exit;
 
 fun exit_result f (x, lthy) =
@@ -372,18 +375,19 @@
 
 (* nested targets *)
 
-fun init_target background_naming operations after_close lthy =
+fun init_target {background_naming, after_close} operations lthy =
   let
     val _ = assert lthy;
     val after_close' = Proof_Context.restore_naming lthy #> after_close;
     val (scope, target) = Proof_Context.new_scope lthy;
     val lthy' =
       target
-      |> Data.map (cons (make_lthy (background_naming, operations, after_close', true, target)));
+      |> Data.map (cons (make_lthy (background_naming, operations, after_close', exit_of lthy, true, target)));
   in (scope, lthy') end;
 
 fun open_target lthy =
-  init_target (background_naming_of lthy) (operations_of lthy) I lthy;
+  init_target {background_naming = background_naming_of lthy, after_close = I}
+    (operations_of lthy) lthy;
 
 fun close_target lthy =
   let
--- a/src/Pure/Isar/locale.ML	Fri Aug 04 21:30:38 2017 +0200
+++ b/src/Pure/Isar/locale.ML	Fri Aug 04 23:07:14 2017 +0200
@@ -88,6 +88,7 @@
   val print_locale: theory -> bool -> xstring * Position.T -> unit
   val print_registrations: Proof.context -> xstring * Position.T -> unit
   val print_dependencies: Proof.context -> bool -> morphism -> (string * morphism) list -> unit
+  val pretty_locale: theory -> bool -> string -> Pretty.T list
   val pretty_locale_deps: theory -> {name: string, parents: string list, body: Pretty.T} list
 end;
 
@@ -699,13 +700,12 @@
       activate_all name thy cons_elem (K (Morphism.transfer_morphism thy)) (empty_idents, [])
       |> snd |> rev;
   in
-    Pretty.block
-      (Pretty.keyword1 "locale" :: Pretty.brk 1 :: pretty_name locale_ctxt name ::
-        maps (fn elem => [Pretty.fbrk, Pretty.chunks (Element.pretty_ctxt locale_ctxt elem)]) elems)
+    Pretty.keyword1 "locale" :: Pretty.brk 1 :: pretty_name locale_ctxt name ::
+      maps (fn elem => [Pretty.fbrk, Pretty.chunks (Element.pretty_ctxt locale_ctxt elem)]) elems
   end;
 
 fun print_locale thy show_facts raw_name =
-  Pretty.writeln (pretty_locale thy show_facts (check thy raw_name));
+  Pretty.writeln (Pretty.block (pretty_locale thy show_facts (check thy raw_name)));
 
 fun print_registrations ctxt raw_name =
   let
@@ -732,7 +732,7 @@
     fun make_node name =
      {name = name,
       parents = map (fst o fst) (dependencies_of thy name),
-      body = pretty_locale thy false name};
+      body = Pretty.block (pretty_locale thy false name)};
     val names = sort_strings (Name_Space.fold_table (cons o #1) (Locales.get thy) []);
   in map make_node names end;
 
--- a/src/Pure/Isar/named_target.ML	Fri Aug 04 21:30:38 2017 +0200
+++ b/src/Pure/Isar/named_target.ML	Fri Aug 04 23:07:14 2017 +0200
@@ -2,7 +2,7 @@
     Author:     Makarius
     Author:     Florian Haftmann, TU Muenchen
 
-Targets for theory, locale, class -- at the bottom the nested structure.
+Targets for theory, locale, class -- at the bottom of the nested structure.
 *)
 
 signature NAMED_TARGET =
@@ -11,7 +11,9 @@
   val locale_of: local_theory -> string option
   val bottom_locale_of: local_theory -> string option
   val class_of: local_theory -> string option
-  val init: (local_theory -> local_theory) option -> string -> theory -> local_theory
+  val init: string -> theory -> local_theory
+  val init': {setup: local_theory -> local_theory, conclude: local_theory -> local_theory} ->
+    string -> theory -> local_theory
   val theory_init: theory -> local_theory
   val theory_map: (local_theory -> local_theory) -> theory -> theory
   val begin: xstring * Position.T -> theory -> local_theory
@@ -25,41 +27,53 @@
 
 (* context data *)
 
+datatype target = Theory | Locale of string | Class of string;
+
+fun target_of_ident _ "" = Theory
+  | target_of_ident thy ident =
+      if Locale.defined thy ident
+      then (if Class.is_class thy ident then Class else Locale) ident
+      else error ("No such locale: " ^ quote ident);
+
+fun ident_of_target Theory = ""
+  | ident_of_target (Locale locale) = locale
+  | ident_of_target (Class class) = class;
+
+fun target_is_theory (SOME Theory) = true
+  | target_is_theory _ = false;
+
+fun locale_of_target (SOME (Locale locale)) = SOME locale
+  | locale_of_target (SOME (Class locale)) = SOME locale
+  | locale_of_target _ = NONE;
+
+fun class_of_target (SOME (Class class)) = SOME class
+  | class_of_target _ = NONE;
+
 structure Data = Proof_Data
 (
-  type T = (string * bool) option;
+  type T = target option;
   fun init _ = NONE;
 );
 
-val get_bottom_data = Data.get;
+val get_bottom_target = Data.get;
 
-fun get_data lthy =
+fun get_target lthy =
   if Local_Theory.level lthy = 1
-  then get_bottom_data lthy
+  then get_bottom_target lthy
   else NONE;
 
-fun is_theory lthy =
-  (case get_data lthy of
-    SOME ("", _) => true
-  | _ => false);
-
-fun target_of lthy =
-  (case get_data lthy of
+fun ident_of lthy =
+  case get_target lthy of
     NONE => error "Not in a named target"
-  | SOME (target, _) => target);
+  | SOME target => ident_of_target target;
 
-fun locale_name_of NONE = NONE
-  | locale_name_of (SOME ("", _)) = NONE
-  | locale_name_of (SOME (locale, _)) = SOME locale;
+val is_theory = target_is_theory o get_target;
 
-val locale_of = locale_name_of o get_data;
+val locale_of = locale_of_target o get_target;
 
-val bottom_locale_of = locale_name_of o get_bottom_data;
+val bottom_locale_of = locale_of_target o get_bottom_target;
 
-fun class_of lthy =
-  (case get_data lthy of
-    SOME (class, true) => SOME class
-  | _ => NONE);
+val class_of = class_of_target o get_target;
 
 
 (* operations *)
@@ -74,94 +88,60 @@
   #-> (fn (lhs, def) => Class.const class ((b, mx), lhs) params
     #> pair (lhs, def));
 
-fun foundation ("", _) = Generic_Target.theory_target_foundation
-  | foundation (locale, false) = locale_foundation locale
-  | foundation (class, true) = class_foundation class;
-
-fun notes ("", _) = Generic_Target.theory_target_notes
-  | notes (locale, _) = Generic_Target.locale_target_notes locale;
-
-fun abbrev ("", _) = Generic_Target.theory_abbrev
-  | abbrev (locale, false) = Generic_Target.locale_abbrev locale
-  | abbrev (class, true) = Class.abbrev class;
-
-fun declaration ("", _) _ decl = Generic_Target.theory_declaration decl
-  | declaration (locale, _) flags decl = Generic_Target.locale_declaration locale flags decl;
-
-fun theory_registration ("", _) = Generic_Target.theory_registration
-  | theory_registration _ = (fn _ => error "Not possible in theory target");
-
-fun locale_dependency ("", false) = (fn _ => error "Not possible in locale target")
-  | locale_dependency ("", true) = (fn _ => error "Not possible in class target")
-  | locale_dependency (locale, _) = Generic_Target.locale_dependency locale;
+fun operations Theory =
+      {define = Generic_Target.define Generic_Target.theory_target_foundation,
+       notes = Generic_Target.notes Generic_Target.theory_target_notes,
+       abbrev = Generic_Target.theory_abbrev,
+       declaration = fn _ => Generic_Target.theory_declaration,
+       theory_registration = Generic_Target.theory_registration,
+       locale_dependency = fn _ => error "Not possible in theory target",
+       pretty = fn ctxt => [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1,
+        Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))]]}
+  | operations (Locale locale) =
+      {define = Generic_Target.define (locale_foundation locale),
+       notes = Generic_Target.notes (Generic_Target.locale_target_notes locale),
+       abbrev = Generic_Target.locale_abbrev locale,
+       declaration = Generic_Target.locale_declaration locale,
+       theory_registration = fn _ => error "Not possible in locale target",
+       locale_dependency = Generic_Target.locale_dependency locale,
+       pretty = fn ctxt => Locale.pretty_locale (Proof_Context.theory_of ctxt) false locale}
+  | operations (Class class) =
+      {define = Generic_Target.define (class_foundation class),
+       notes = Generic_Target.notes (Generic_Target.locale_target_notes class),
+       abbrev = Class.abbrev class,
+       declaration = Generic_Target.locale_declaration class,
+       theory_registration = fn _ => error "Not possible in class target",
+       locale_dependency = Generic_Target.locale_dependency class,
+       pretty = fn ctxt => Class.pretty_specification (Proof_Context.theory_of ctxt) class};
 
-fun pretty (target, is_class) ctxt =
-  if target = "" then
-    [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1,
-      Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))]]
-  else if is_class then Class.pretty_specification (Proof_Context.theory_of ctxt) target
-  else
-    (* FIXME pretty locale content *)
-    let
-      val target_name = [Pretty.keyword1 "locale", Pretty.brk 1, Locale.pretty_name ctxt target];
-      val fixes =
-        map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
-          (#1 (Proof_Context.inferred_fixes ctxt));
-      val assumes =
-        map (fn A => (Binding.empty_atts, [(Thm.term_of A, [])]))
-          (Assumption.all_assms_of ctxt);
-      val elems =
-        (if null fixes then [] else [Element.Fixes fixes]) @
-        (if null assumes then [] else [Element.Assumes assumes]);
-    in
-      if null elems then [Pretty.block target_name]
-      else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) ::
-        map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))]
-    end;
+fun setup_context Theory = Proof_Context.init_global
+  | setup_context (Locale locale) = Locale.init locale
+  | setup_context (Class class) = Class.init class;
 
-
-(* init *)
-
-fun make_name_data _ "" = ("", false)
-  | make_name_data thy target =
-      if Locale.defined thy target
-      then (target, Class.is_class thy target)
-      else error ("No such locale: " ^ quote target);
-
-fun init_context ("", _) = Proof_Context.init_global
-  | init_context (locale, false) = Locale.init locale
-  | init_context (class, true) = Class.init class;
-
-fun init before_exit target thy =
+fun init' {setup, conclude} ident thy =
   let
-    val name_data = make_name_data thy target;
-    val background_naming =
-      Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name target);
+    val target = target_of_ident thy ident;
   in
     thy
-    |> Sign.change_begin
-    |> init_context name_data
-    |> is_none before_exit ? Data.put (SOME name_data)
-    |> Local_Theory.init background_naming
-       {define = Generic_Target.define (foundation name_data),
-        notes = Generic_Target.notes (notes name_data),
-        abbrev = abbrev name_data,
-        declaration = declaration name_data,
-        theory_registration = theory_registration name_data,
-        locale_dependency = locale_dependency name_data,
-        pretty = pretty name_data,
-        exit = the_default I before_exit
-          #> Local_Theory.target_of #> Sign.change_end_local}
+    |> Generic_Target.init
+       {background_naming = Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name ident),
+        setup = setup_context target #> setup,
+        conclude = conclude}
+       (operations target)
   end;
 
-val theory_init = init NONE "";
+fun init ident thy =
+  init' {setup = Data.put (SOME (target_of_ident thy ident)), conclude = I} ident thy;
+
+val theory_init = init "";
+
 fun theory_map f = theory_init #> f #> Local_Theory.exit_global;
 
 
 (* toplevel interaction *)
 
 fun begin ("-", _) thy = theory_init thy
-  | begin target thy = init NONE (Locale.check thy target) thy;
+  | begin target thy = init (Locale.check thy target) thy;
 
 val exit = Local_Theory.assert_bottom #> Local_Theory.exit_global;
 
@@ -172,7 +152,7 @@
   | switch NONE (Context.Proof lthy) =
       (Context.Proof o Local_Theory.reset, lthy)
   | switch (SOME name) (Context.Proof lthy) =
-      (Context.Proof o init NONE (target_of lthy) o exit,
+      (Context.Proof o init (ident_of lthy) o exit,
         (begin name o exit o Local_Theory.assert_nonbrittle) lthy);
 
 end;
--- a/src/Pure/Isar/overloading.ML	Fri Aug 04 21:30:38 2017 +0200
+++ b/src/Pure/Isar/overloading.ML	Fri Aug 04 23:07:14 2017 +0200
@@ -193,21 +193,21 @@
       (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 (Sign.naming_of thy)
+    |> Generic_Target.init
+       {background_naming = Sign.naming_of thy,
+        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,
         declaration = K Generic_Target.theory_declaration,
         theory_registration = Generic_Target.theory_registration,
         locale_dependency = fn _ => error "Not possible in overloading target",
-        pretty = pretty,
-        exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
+        pretty = pretty}
   end;
 
 val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
--- a/src/Tools/Code/code_preproc.ML	Fri Aug 04 21:30:38 2017 +0200
+++ b/src/Tools/Code/code_preproc.ML	Fri Aug 04 23:07:14 2017 +0200
@@ -306,7 +306,9 @@
     AList.make (snd o Graph.get_node eqngr) (Graph.keys eqngr)
     |> (map o apfst) (Code.string_of_const thy)
     |> sort (string_ord o apply2 fst)
-    |> map (fn (s, cert) => (Pretty.block o Pretty.fbreaks) (Pretty.str s :: Code.pretty_cert thy cert))
+    |> (map o apsnd) (Code.pretty_cert thy)
+    |> filter_out (null o snd)
+    |> map (fn (s, ps) => (Pretty.block o Pretty.fbreaks) (Pretty.str s :: ps))
     |> Pretty.chunks
   end;