equal
deleted
inserted
replaced
79 val amend_registration: registration -> Context.generic -> Context.generic |
79 val amend_registration: registration -> Context.generic -> Context.generic |
80 val add_registration: registration -> Context.generic -> Context.generic |
80 val add_registration: registration -> Context.generic -> Context.generic |
81 val add_registration_theory: registration -> theory -> theory |
81 val add_registration_theory: registration -> theory -> theory |
82 val add_registration_proof: registration -> Proof.context -> Proof.context |
82 val add_registration_proof: registration -> Proof.context -> Proof.context |
83 val add_registration_local_theory: registration -> local_theory -> local_theory |
83 val add_registration_local_theory: registration -> local_theory -> local_theory |
84 val activate_fragment: registration -> local_theory -> local_theory |
|
85 val registrations_of: Context.generic -> string -> (string * morphism) list |
84 val registrations_of: Context.generic -> string -> (string * morphism) list |
86 val add_dependency: string -> registration -> theory -> theory |
85 val add_dependency: string -> registration -> theory -> theory |
87 |
86 |
88 (* Diagnostic *) |
87 (* Diagnostic *) |
89 val get_locales: theory -> string list |
88 val get_locales: theory -> string list |
572 lthy |> Local_Theory.map_contexts (fn level => |
571 lthy |> Local_Theory.map_contexts (fn level => |
573 level = n - 1 ? Context.proof_map (add_registration registration)) |
572 level = n - 1 ? Context.proof_map (add_registration registration)) |
574 end; |
573 end; |
575 |
574 |
576 |
575 |
577 (* locale fragments within local theory *) |
|
578 |
|
579 fun activate_fragment registration = |
|
580 Local_Theory.mark_brittle #> add_registration_local_theory registration; |
|
581 |
|
582 |
|
583 |
576 |
584 (*** Dependencies ***) |
577 (*** Dependencies ***) |
585 |
578 |
586 fun add_dependency loc {dep = (name, morph), mixin, export} thy = |
579 fun add_dependency loc {dep = (name, morph), mixin, export} thy = |
587 let |
580 let |