--- 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;