--- a/src/Pure/Isar/class.ML Sat Oct 24 14:40:12 2020 +0000
+++ b/src/Pure/Isar/class.ML Sat Oct 24 15:16:54 2020 +0000
@@ -493,7 +493,7 @@
val add_dependency =
(case some_dep_morph of
SOME dep_morph =>
- Generic_Target.locale_dependency sub
+ Locale.add_dependency sub
{inst = (sup, dep_morph $> Element.satisfy_morphism (the_list some_witn)),
mixin = NONE, export = export}
| NONE => I);
@@ -710,7 +710,7 @@
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,
+ theory_registration = Locale.add_registration_theory,
locale_dependency = fn _ => error "Not possible in instantiation target",
pretty = pretty}
end;
--- a/src/Pure/Isar/class_declaration.ML Sat Oct 24 14:40:12 2020 +0000
+++ b/src/Pure/Isar/class_declaration.ML Sat Oct 24 15:16:54 2020 +0000
@@ -327,7 +327,7 @@
|-> (fn (param_map, params, assm_axiom) =>
`(fn thy => calculate thy class sups base_sort param_map assm_axiom)
#-> (fn (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) =>
- Locale.add_registration_theory
+ Locale.add_registration_theory'
{inst = (class, base_morph),
mixin = Option.map (rpair true) eq_morph,
export = export_morph}
--- a/src/Pure/Isar/generic_target.ML Sat Oct 24 14:40:12 2020 +0000
+++ b/src/Pure/Isar/generic_target.ML Sat Oct 24 15:16:54 2020 +0000
@@ -54,7 +54,6 @@
val theory_abbrev: Syntax.mode -> (binding * mixfix) * term ->
local_theory -> (term * term) * local_theory
val theory_declaration: declaration -> local_theory -> local_theory
- val theory_registration: Locale.registration -> local_theory -> local_theory
(*locale target primitives*)
val locale_target_notes: string -> string -> Attrib.fact list -> Attrib.fact list ->
@@ -72,7 +71,6 @@
local_theory -> local_theory
val locale_const: string -> Syntax.mode -> (binding * mixfix) * term ->
local_theory -> local_theory
- val locale_dependency: string -> Locale.registration -> local_theory -> local_theory
(*initialisation*)
val init: {background_naming: Name_Space.naming, setup: theory -> Proof.context,
@@ -400,10 +398,6 @@
fun theory_declaration decl =
background_declaration decl #> standard_declaration (K true) decl;
-val theory_registration =
- Local_Theory.raw_theory o Locale.add_registration_theory;
-
-
(** locale target primitives **)
@@ -435,10 +429,6 @@
locale_target_const locale (K true) prmode ((b, mx), rhs)
#> standard_const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs);
-fun locale_dependency locale registration =
- Local_Theory.raw_theory (Locale.add_dependency locale registration)
- #> Locale.add_registration_local_theory registration;
-
(** locale abbreviations **)
--- a/src/Pure/Isar/interpretation.ML Sat Oct 24 14:40:12 2020 +0000
+++ b/src/Pure/Isar/interpretation.ML Sat Oct 24 15:16:54 2020 +0000
@@ -156,16 +156,13 @@
(* interpretation in local theories *)
-fun activate_fragment registration =
- Local_Theory.mark_brittle #> Locale.add_registration_local_theory registration;
-
fun interpretation expression =
generic_interpretation cert_interpretation Element.witness_proof_eqs
- Local_Theory.notes_kind activate_fragment expression [];
+ Local_Theory.notes_kind Locale.add_registration_local_theory expression [];
fun interpretation_cmd expression =
generic_interpretation read_interpretation Element.witness_proof_eqs
- Local_Theory.notes_kind activate_fragment expression [];
+ Local_Theory.notes_kind Locale.add_registration_local_theory expression [];
(* interpretation into global theories *)
@@ -222,7 +219,7 @@
fun register_or_activate lthy =
if Named_Target.is_theory lthy
then Local_Theory.theory_registration
- else activate_fragment;
+ else Locale.add_registration_local_theory;
fun gen_isar_interpretation prep_interpretation expression lthy =
generic_interpretation prep_interpretation Element.witness_proof_eqs
--- a/src/Pure/Isar/local_theory.ML Sat Oct 24 14:40:12 2020 +0000
+++ b/src/Pure/Isar/local_theory.ML Sat Oct 24 15:16:54 2020 +0000
@@ -24,9 +24,7 @@
type operations
val assert: local_theory -> local_theory
val level: Proof.context -> int
- val assert_bottom: local_theory -> local_theory
val mark_brittle: local_theory -> local_theory
- val assert_nonbrittle: local_theory -> local_theory
val map_contexts: (int -> Proof.context -> Proof.context) -> local_theory -> local_theory
val background_naming_of: local_theory -> Name_Space.naming
val map_background_naming: (Name_Space.naming -> Name_Space.naming) ->
@@ -71,6 +69,7 @@
operations -> Proof.context -> local_theory
val exit: local_theory -> Proof.context
val exit_global: local_theory -> theory
+ val exit_global_nonbrittle: 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 begin_nested: local_theory -> Binding.scope * local_theory
@@ -363,6 +362,7 @@
fun exit lthy = exit_of lthy (assert_bottom lthy);
val exit_global = Proof_Context.theory_of o exit;
+val exit_global_nonbrittle = exit_global o assert_nonbrittle;
fun exit_result decl (x, lthy) =
let
--- a/src/Pure/Isar/locale.ML Sat Oct 24 14:40:12 2020 +0000
+++ b/src/Pure/Isar/locale.ML Sat Oct 24 15:16:54 2020 +0000
@@ -79,11 +79,13 @@
type registration = {inst: string * morphism, mixin: (morphism * bool) option, export: morphism}
val amend_registration: registration -> Context.generic -> Context.generic
val add_registration: registration -> Context.generic -> Context.generic
- val add_registration_theory: registration -> theory -> theory
- val add_registration_proof: registration -> Proof.context -> Proof.context
+ val add_registration_theory': registration -> theory -> theory
+ val add_registration_theory: registration -> local_theory -> local_theory
val add_registration_local_theory: registration -> local_theory -> local_theory
+ val add_registration_proof: registration -> Proof.context -> Proof.context
val registrations_of: Context.generic -> string -> (string * morphism) list
- val add_dependency: string -> registration -> theory -> theory
+ val add_dependency': string -> registration -> theory -> theory
+ val add_dependency: string -> registration -> local_theory -> local_theory
(* Diagnostic *)
val get_locales: theory -> string list
@@ -609,20 +611,25 @@
|> activate_facts (SOME export) (name, mix_morph $> pos_morph)
end;
-val add_registration_theory = Context.theory_map o add_registration;
+val add_registration_theory' = Context.theory_map o add_registration;
+
+val add_registration_theory = Local_Theory.raw_theory o add_registration_theory';
+
+fun add_registration_local_theory' registration lthy =
+ let val n = Local_Theory.level lthy in
+ lthy
+ |> Local_Theory.map_contexts (fn level =>
+ level = n - 1 ? Context.proof_map (add_registration registration))
+ end;
+
+fun add_registration_local_theory registration =
+ Local_Theory.mark_brittle #> add_registration_local_theory' registration
fun add_registration_proof registration ctxt = ctxt
|> Proof_Context.set_stmt false
|> Context.proof_map (add_registration registration)
|> Proof_Context.restore_stmt ctxt;
-fun add_registration_local_theory registration lthy =
- let val n = Local_Theory.level lthy in
- lthy |> Local_Theory.map_contexts (fn level =>
- level = n - 1 ? Context.proof_map (add_registration registration))
- end;
-
-
(*** Dependencies ***)
@@ -633,7 +640,7 @@
|> map (fn (name, (base, export)) =>
(name, base $> (collect_mixins context (name, base $> export)) $> export));
-fun add_dependency loc {inst = (name, morph), mixin, export} thy =
+fun add_dependency' loc {inst = (name, morph), mixin, export} thy =
let
val dep = make_dep (name, (morph, export));
val add_dep =
@@ -645,10 +652,14 @@
fold_rev (roundup thy' cons export)
(registrations_of context' loc) (Idents.get context', []);
in
- fold_rev (fn inst => add_registration_theory {inst = inst, mixin = NONE, export = export})
+ fold_rev (fn inst => add_registration_theory' {inst = inst, mixin = NONE, export = export})
regs thy'
end;
+fun add_dependency loc registration =
+ Local_Theory.raw_theory (add_dependency' loc registration)
+ #> add_registration_local_theory' registration;
+
(*** Storing results ***)
--- a/src/Pure/Isar/named_target.ML Sat Oct 24 14:40:12 2020 +0000
+++ b/src/Pure/Isar/named_target.ML Sat Oct 24 15:16:54 2020 +0000
@@ -92,7 +92,7 @@
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,
+ theory_registration = Locale.add_registration_theory,
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))]]}
@@ -102,7 +102,7 @@
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,
+ locale_dependency = Locale.add_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),
@@ -110,7 +110,7 @@
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,
+ locale_dependency = Locale.add_dependency class,
pretty = fn ctxt => Class.pretty_specification (Proof_Context.theory_of ctxt) class};
fun setup_context Theory = Proof_Context.init_global
--- a/src/Pure/Isar/overloading.ML Sat Oct 24 14:40:12 2020 +0000
+++ b/src/Pure/Isar/overloading.ML Sat Oct 24 15:16:54 2020 +0000
@@ -210,7 +210,7 @@
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,
+ theory_registration = Locale.add_registration_theory,
locale_dependency = fn _ => error "Not possible in overloading target",
pretty = pretty}
end;
--- a/src/Pure/Isar/target_context.ML Sat Oct 24 14:40:12 2020 +0000
+++ b/src/Pure/Isar/target_context.ML Sat Oct 24 15:16:54 2020 +0000
@@ -7,7 +7,7 @@
signature TARGET_CONTEXT =
sig
val context_begin_named_cmd: xstring * Position.T -> theory -> local_theory
- val end_named_cmd: local_theory -> theory
+ val end_named_cmd: local_theory -> Context.generic
val switch_named_cmd: (xstring * Position.T) option -> Context.generic ->
(local_theory -> Context.generic) * local_theory
val context_begin_nested_cmd: (xstring * Position.T) list -> Element.context list ->
@@ -21,17 +21,17 @@
fun context_begin_named_cmd ("-", _) thy = Named_Target.theory_init thy
| context_begin_named_cmd target thy = Named_Target.init (Locale.check thy target) thy;
-val end_named_cmd = Local_Theory.exit_global;
+val end_named_cmd = Context.Theory o Local_Theory.exit_global;
fun switch_named_cmd NONE (Context.Theory thy) =
- (Context.Theory o end_named_cmd, Named_Target.theory_init thy)
+ (Context.Theory o Local_Theory.exit_global, Named_Target.theory_init thy)
| switch_named_cmd (SOME name) (Context.Theory thy) =
- (Context.Theory o end_named_cmd, context_begin_named_cmd name thy)
+ (Context.Theory o Local_Theory.exit_global, context_begin_named_cmd name thy)
| switch_named_cmd NONE (Context.Proof lthy) =
(Context.Proof o Local_Theory.reset, lthy)
| switch_named_cmd (SOME name) (Context.Proof lthy) =
- (Context.Proof o Named_Target.reinit lthy o end_named_cmd,
- (context_begin_named_cmd name o end_named_cmd o Local_Theory.assert_nonbrittle) lthy);
+ (Context.Proof o Named_Target.reinit lthy o Local_Theory.exit_global,
+ (context_begin_named_cmd name o Local_Theory.exit_global_nonbrittle) lthy);
fun includes raw_incls lthy =
Bundle.includes (map (Bundle.check lthy) raw_incls) lthy;
@@ -45,10 +45,14 @@
|> Local_Theory.begin_nested
|> snd;
-fun end_nested_cmd lthy =
- if Named_Target.is_theory lthy
- then Context.Theory (Local_Theory.exit_global lthy)
- else Context.Proof lthy;
+fun end_nested_cmd lthy =
+ let
+ val lthy' = Local_Theory.end_nested lthy
+ in
+ if Named_Target.is_theory lthy'
+ then Context.Theory (Local_Theory.exit_global lthy')
+ else Context.Proof lthy'
+ end;
end;
--- a/src/Pure/Isar/toplevel.ML Sat Oct 24 14:40:12 2020 +0000
+++ b/src/Pure/Isar/toplevel.ML Sat Oct 24 15:16:54 2020 +0000
@@ -439,7 +439,7 @@
val gthy =
if begin
then Context.Proof lthy
- else Context.Theory (Target_Context.end_named_cmd lthy);
+ else Target_Context.end_named_cmd lthy;
val _ =
(case Local_Theory.pretty lthy of
[] => ()
@@ -448,7 +448,7 @@
| _ => raise UNDEF));
val end_main_target = transaction (fn _ =>
- (fn Theory (Context.Proof lthy) => (Theory (Context.Theory (Target_Context.end_named_cmd lthy)), lthy)
+ (fn Theory (Context.Proof lthy) => (Theory (Target_Context.end_named_cmd lthy), lthy)
| _ => raise UNDEF));
fun begin_nested_target f = transaction0 (fn _ =>
@@ -460,10 +460,8 @@
val end_nested_target = transaction (fn _ =>
(fn Theory (Context.Proof lthy) =>
- (case try Local_Theory.end_nested lthy of
- SOME lthy' =>
- let val gthy' = Target_Context.end_nested_cmd lthy'
- in (Theory gthy', lthy) end
+ (case try Target_Context.end_nested_cmd lthy of
+ SOME gthy' => (Theory gthy', lthy)
| NONE => raise UNDEF)
| _ => raise UNDEF));