# HG changeset patch # User paulson # Date 1501880834 -7200 # Node ID 91257fbcabeeaa1b4dbabc945aff0f58828f2fbc # Parent 1a8441ec5cedb5d53350bc5e5d514912a74c8dd9# Parent 1c5e521a98f1dc9105cfbbdf4594b851ff238619 merged diff -r 1c5e521a98f1 -r 91257fbcabee src/Doc/Implementation/Local_Theory.thy --- 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 \ \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 -> diff -r 1c5e521a98f1 -r 91257fbcabee src/HOL/Statespace/state_space.ML --- 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; diff -r 1c5e521a98f1 -r 91257fbcabee src/Pure/Isar/bundle.ML --- 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 diff -r 1c5e521a98f1 -r 91257fbcabee src/Pure/Isar/class.ML --- 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 = diff -r 1c5e521a98f1 -r 91257fbcabee src/Pure/Isar/class_declaration.ML --- 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; diff -r 1c5e521a98f1 -r 91257fbcabee src/Pure/Isar/code.ML --- 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 diff -r 1c5e521a98f1 -r 91257fbcabee src/Pure/Isar/expression.ML --- 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; diff -r 1c5e521a98f1 -r 91257fbcabee src/Pure/Isar/generic_target.ML --- 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; diff -r 1c5e521a98f1 -r 91257fbcabee src/Pure/Isar/interpretation.ML --- 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); diff -r 1c5e521a98f1 -r 91257fbcabee src/Pure/Isar/local_theory.ML --- 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 diff -r 1c5e521a98f1 -r 91257fbcabee src/Pure/Isar/locale.ML --- 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; diff -r 1c5e521a98f1 -r 91257fbcabee src/Pure/Isar/named_target.ML --- 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; diff -r 1c5e521a98f1 -r 91257fbcabee src/Pure/Isar/overloading.ML --- 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); diff -r 1c5e521a98f1 -r 91257fbcabee src/Tools/Code/code_preproc.ML --- 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;