# HG changeset patch # User wenzelm # Date 1407955399 -7200 # Node ID 3b4deb99a932ecb7ecf0bd21a845be1a0949ef7d # Parent dc78785427d05a0d8223dc182f585556e8e0c6f7# Parent c5063c033a5afbd61693ae7da61c0cbadeb30f4e merged diff -r dc78785427d0 -r 3b4deb99a932 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Wed Aug 13 17:17:51 2014 +0200 +++ b/src/Pure/Isar/attrib.ML Wed Aug 13 20:43:19 2014 +0200 @@ -11,6 +11,10 @@ val empty_binding: binding val is_empty_binding: binding -> bool val print_attributes: Proof.context -> unit + val define_global: Binding.binding -> (Args.src -> attribute) -> + string -> theory -> string * theory + val define: Binding.binding -> (Args.src -> attribute) -> + string -> local_theory -> string * local_theory val check_name_generic: Context.generic -> xstring * Position.T -> string val check_name: Proof.context -> xstring * Position.T -> string val check_src: Proof.context -> src -> src @@ -35,6 +39,8 @@ Context.generic -> (string * thm list) list * Context.generic val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory + val local_setup: Binding.binding -> attribute context_parser -> string -> + local_theory -> local_theory val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory val internal: (morphism -> attribute) -> src val add_del: attribute -> attribute -> attribute context_parser @@ -74,7 +80,6 @@ (* source and bindings *) type src = Args.src; - type binding = binding * src list; val empty_binding: binding = (Binding.empty, []); @@ -86,7 +91,7 @@ (* theory data *) -structure Attributes = Theory_Data +structure Attributes = Generic_Data ( type T = ((src -> attribute) * string) Name_Space.table; val empty : T = Name_Space.empty_table "attribute"; @@ -94,11 +99,17 @@ fun merge data : T = Name_Space.merge_tables data; ); -val get_attributes = Attributes.get o Context.theory_of; +val get_attributes = Attributes.get o Context.Proof; + +fun transfer_attributes thy ctxt = + let + val attribs' = + Name_Space.merge_tables (Attributes.get (Context.Theory thy), get_attributes ctxt); + in Context.proof_map (Attributes.put attribs') ctxt end; fun print_attributes ctxt = let - val attribs = get_attributes (Context.Proof ctxt); + val attribs = get_attributes ctxt; fun prt_attr (name, (_, "")) = Pretty.mark_str name | prt_attr (name, (_, comment)) = Pretty.block @@ -108,20 +119,46 @@ |> Pretty.writeln_chunks end; -val attribute_space = Name_Space.space_of_table o get_attributes o Context.Proof; +val attribute_space = Name_Space.space_of_table o get_attributes; + + +(* define *) + +fun define_global binding att comment thy = + let + val context = Context.Theory thy; + val (name, attribs') = + Name_Space.define context true (binding, (att, comment)) (Attributes.get context); + in (name, Context.the_theory (Attributes.put attribs' context)) end; -fun add_attribute name att comment thy = thy - |> Attributes.map (Name_Space.define (Context.Theory thy) true (name, (att, comment)) #> snd); +fun define binding att comment lthy = + let + val standard_morphism = + Local_Theory.standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy)); + val att0 = att o Args.transform_values standard_morphism; + in + lthy + |> Local_Theory.background_theory_result (define_global binding att0 comment) + |-> (fn name => + Local_Theory.map_contexts + (fn _ => fn ctxt => transfer_attributes (Proof_Context.theory_of ctxt) ctxt) + #> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context => + let + val naming = Name_Space.naming_of context; + val binding' = Morphism.binding phi binding; + in Attributes.map (Name_Space.alias_table naming binding' name) context end) + #> pair name) + end; (* check *) -fun check_name_generic context = #1 o Name_Space.check context (get_attributes context); +fun check_name_generic context = #1 o Name_Space.check context (Attributes.get context); val check_name = check_name_generic o Context.Proof; fun check_src ctxt src = (Context_Position.report ctxt (Args.range_of_src src) Markup.language_attribute; - #1 (Args.check_src ctxt (get_attributes (Context.Proof ctxt)) src)); + #1 (Args.check_src ctxt (get_attributes ctxt) src)); (* pretty printing *) @@ -133,7 +170,7 @@ (* get attributes *) fun attribute_generic context = - let val table = get_attributes context + let val table = Attributes.get context in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end; val attribute = attribute_generic o Context.Proof; @@ -171,10 +208,11 @@ (* attribute setup *) -fun setup name scan = - add_attribute name - (fn src => fn (ctxt, th) => - let val (a, ctxt') = Args.syntax_generic scan src ctxt in a (ctxt', th) end); +fun attribute_syntax scan src (context, th) = + let val (a, context') = Args.syntax_generic scan src context in a (context', th) end; + +fun setup binding scan comment = define_global binding (attribute_syntax scan) comment #> snd; +fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd; fun attribute_setup name source cmt = Context.theory_map (ML_Context.expression (#pos source) diff -r dc78785427d0 -r 3b4deb99a932 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Wed Aug 13 17:17:51 2014 +0200 +++ b/src/Pure/Isar/expression.ML Wed Aug 13 20:43:19 2014 +0200 @@ -924,7 +924,7 @@ fun subscribe_or_activate lthy = if Named_Target.is_theory lthy then Local_Theory.subscription - else Local_Theory.activate; + else Locale.activate_fragment; fun subscribe_locale_only lthy = let @@ -964,7 +964,7 @@ (K Local_Theory.subscription) expression raw_eqns; fun ephemeral_interpretation x = - gen_local_theory_interpretation cert_interpretation (K Local_Theory.activate) x; + gen_local_theory_interpretation cert_interpretation (K Locale.activate_fragment) x; fun interpretation x = gen_local_theory_interpretation cert_interpretation subscribe_or_activate x; diff -r dc78785427d0 -r 3b4deb99a932 src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Wed Aug 13 17:17:51 2014 +0200 +++ b/src/Pure/Isar/generic_target.ML Wed Aug 13 20:43:19 2014 +0200 @@ -358,6 +358,6 @@ fun locale_dependency locale dep_morph mixin export = (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export - #> Local_Theory.activate_nonbrittle dep_morph mixin export; + #> Locale.activate_fragment_nonbrittle dep_morph mixin export; end; diff -r dc78785427d0 -r 3b4deb99a932 src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Wed Aug 13 17:17:51 2014 +0200 +++ b/src/Pure/Isar/local_theory.ML Wed Aug 13 20:43:19 2014 +0200 @@ -7,6 +7,12 @@ type local_theory = Proof.context; type generic_theory = Context.generic; +structure Attrib = +struct + type src = Args.src; + type binding = binding * src list; +end; + signature LOCAL_THEORY = sig type operations @@ -14,6 +20,7 @@ val restore: local_theory -> local_theory val level: Proof.context -> int val assert_bottom: bool -> local_theory -> local_theory + val mark_brittle: local_theory -> local_theory val assert_nonbrittle: local_theory -> local_theory val open_target: Name_Space.naming -> operations -> (local_theory -> local_theory) -> local_theory -> local_theory @@ -52,16 +59,13 @@ val subscription: string * morphism -> (morphism * bool) option -> morphism -> local_theory -> local_theory val pretty: local_theory -> Pretty.T list + val add_thms_dynamic: binding * (Context.generic -> thm list) -> local_theory -> local_theory val set_defsort: sort -> local_theory -> local_theory val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory val class_alias: binding -> class -> local_theory -> local_theory val type_alias: binding -> string -> local_theory -> local_theory val const_alias: binding -> string -> local_theory -> local_theory - val activate: string * morphism -> (morphism * bool) option -> morphism -> - local_theory -> local_theory - val activate_nonbrittle: string * morphism -> (morphism * bool) option -> morphism -> - local_theory -> local_theory val init: Name_Space.naming -> operations -> Proof.context -> local_theory val exit: local_theory -> Proof.context val exit_global: local_theory -> theory @@ -115,7 +119,7 @@ val bottom_of = List.last o Data.get o assert; val top_of = hd o Data.get o assert; -fun map_bottom f = +fun map_top f = assert #> Data.map (fn {naming, operations, after_close, brittle, target} :: parents => make_lthy (f (naming, operations, after_close, brittle, target)) :: parents); @@ -162,14 +166,13 @@ (* brittle context -- implicit for nested structures *) fun mark_brittle lthy = - if level lthy = 1 - then map_bottom (fn (naming, operations, after_close, brittle, target) => - (naming, operations, after_close, true, target)) lthy + if level lthy = 1 then + map_top (fn (naming, operations, after_close, brittle, target) => + (naming, operations, after_close, true, target)) lthy else lthy; fun assert_nonbrittle lthy = - if #brittle (top_of lthy) - then error "Brittle local theory context" + if #brittle (top_of lthy) then error "Brittle local theory context" else lthy; @@ -179,7 +182,7 @@ val full_name = Name_Space.full_name o naming_of; fun map_naming f = - map_bottom (fn (naming, operations, after_close, brittle, target) => + map_top (fn (naming, operations, after_close, brittle, target) => (f naming, operations, after_close, brittle, target)); val conceal = map_naming Name_Space.conceal; @@ -272,6 +275,20 @@ val notes = notes_kind ""; fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single; +fun add_thms_dynamic (binding, f) lthy = + lthy + |> background_theory_result (fn thy => thy + |> Global_Theory.add_thms_dynamic' (Sign.inherit_naming thy lthy) (binding, f)) + |-> (fn name => + map_contexts (fn _ => fn ctxt => + Proof_Context.transfer_facts (Proof_Context.theory_of ctxt) ctxt) #> + declaration {syntax = false, pervasive = false} (fn phi => + let val binding' = Morphism.binding phi binding in + Context.mapping + (Global_Theory.alias_fact binding' name) + (Proof_Context.fact_alias binding' name) + end)); + fun set_defsort S = declaration {syntax = true, pervasive = false} (K (Context.mapping (Sign.set_defsort S) (Proof_Context.set_defsort S))); @@ -308,17 +325,6 @@ val const_alias = alias Sign.const_alias Proof_Context.const_alias; -(* activation of locale fragments *) - -fun activate_nonbrittle dep_morph mixin export = - map_bottom (fn (naming, operations, after_close, brittle, target) => - (naming, operations, after_close, brittle, - (Context.proof_map ooo Locale.add_registration) dep_morph mixin export target)); - -fun activate dep_morph mixin export = - mark_brittle #> activate_nonbrittle dep_morph mixin export; - - (** init and exit **) diff -r dc78785427d0 -r 3b4deb99a932 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Wed Aug 13 17:17:51 2014 +0200 +++ b/src/Pure/Isar/locale.ML Wed Aug 13 20:43:19 2014 +0200 @@ -70,6 +70,10 @@ (* Registrations and dependencies *) val add_registration: string * morphism -> (morphism * bool) option -> morphism -> Context.generic -> Context.generic + val activate_fragment: string * morphism -> (morphism * bool) option -> morphism -> + local_theory -> local_theory + val activate_fragment_nonbrittle: string * morphism -> (morphism * bool) option -> morphism -> + local_theory -> local_theory val amend_registration: string * morphism -> morphism * bool -> morphism -> Context.generic -> Context.generic val registrations_of: Context.generic -> string -> (string * morphism) list @@ -514,6 +518,19 @@ end; +(* locale fragments within local theory *) + +fun activate_fragment_nonbrittle dep_morph mixin export lthy = + let val n = Local_Theory.level lthy in + lthy |> Local_Theory.map_contexts (fn level => + level = n - 1 ? Context.proof_map (add_registration dep_morph mixin export)) + end; + +fun activate_fragment dep_morph mixin export = + Local_Theory.mark_brittle #> activate_fragment_nonbrittle dep_morph mixin export; + + + (*** Dependencies ***) (* FIXME dead code!? diff -r dc78785427d0 -r 3b4deb99a932 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Wed Aug 13 17:17:51 2014 +0200 +++ b/src/Pure/Isar/proof_context.ML Wed Aug 13 20:43:19 2014 +0200 @@ -50,6 +50,7 @@ val markup_const: Proof.context -> string -> string val pretty_const: Proof.context -> string -> Pretty.T val transfer: theory -> Proof.context -> Proof.context + val transfer_facts: theory -> Proof.context -> Proof.context val background_theory: (theory -> theory) -> Proof.context -> Proof.context val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context val facts_of: Proof.context -> Facts.T @@ -323,16 +324,19 @@ map_tsig (fn tsig as (local_tsig, global_tsig) => let val thy_tsig = Sign.tsig_of thy in if Type.eq_tsig (thy_tsig, global_tsig) then tsig - else (Type.merge_tsig (Context.pretty ctxt) (local_tsig, thy_tsig), thy_tsig) + else (Type.merge_tsig (Context.pretty ctxt) (local_tsig, thy_tsig), thy_tsig) (*historic merge order*) end) |> map_consts (fn consts as (local_consts, global_consts) => let val thy_consts = Sign.consts_of thy in if Consts.eq_consts (thy_consts, global_consts) then consts - else (Consts.merge (local_consts, thy_consts), thy_consts) + else (Consts.merge (local_consts, thy_consts), thy_consts) (*historic merge order*) end); fun transfer thy = Context.raw_transfer thy #> transfer_syntax thy; +fun transfer_facts thy = + map_facts (fn local_facts => Facts.merge (Global_Theory.facts_of thy, local_facts)); + fun background_theory f ctxt = transfer (f (theory_of ctxt)) ctxt; fun background_theory_result f ctxt = diff -r dc78785427d0 -r 3b4deb99a932 src/Pure/PIDE/prover.scala --- a/src/Pure/PIDE/prover.scala Wed Aug 13 17:17:51 2014 +0200 +++ b/src/Pure/PIDE/prover.scala Wed Aug 13 20:43:19 2014 +0200 @@ -1,7 +1,8 @@ /* Title: Pure/PIDE/prover.scala Author: Makarius + Options: :folding=explicit: -General prover operations and process wrapping. +Prover process wrapping. */ package isabelle @@ -87,7 +88,7 @@ system_channel: System_Channel, system_process: Prover.System_Process) extends Protocol { - /* output */ + /** receiver output **/ val xml_cache: XML.Cache = new XML.Cache() diff -r dc78785427d0 -r 3b4deb99a932 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Wed Aug 13 17:17:51 2014 +0200 +++ b/src/Pure/PIDE/session.scala Wed Aug 13 20:43:19 2014 +0200 @@ -1,6 +1,6 @@ /* Title: Pure/PIDE/session.scala Author: Makarius - Options: :folding=explicit:collapseFolds=1: + Options: :folding=explicit: PIDE editor session, potentially with running prover process. */ diff -r dc78785427d0 -r 3b4deb99a932 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Aug 13 17:17:51 2014 +0200 +++ b/src/Pure/ROOT.ML Wed Aug 13 20:43:19 2014 +0200 @@ -234,7 +234,8 @@ use "Isar/parse.ML"; use "Isar/args.ML"; -(*theory sources*) +(*theory specifications*) +use "Isar/local_theory.ML"; use "Thy/thy_header.ML"; use "PIDE/command_span.ML"; use "Thy/thy_syntax.ML"; @@ -264,7 +265,6 @@ (*local theories and targets*) use "Isar/locale.ML"; -use "Isar/local_theory.ML"; use "Isar/generic_target.ML"; use "Isar/overloading.ML"; use "axclass.ML"; diff -r dc78785427d0 -r 3b4deb99a932 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed Aug 13 17:17:51 2014 +0200 +++ b/src/Pure/Tools/build.scala Wed Aug 13 20:43:19 2014 +0200 @@ -1,6 +1,6 @@ /* Title: Pure/Tools/build.scala Author: Makarius - Options: :folding=explicit:collapseFolds=1: + Options: :folding=explicit: Build and manage Isabelle sessions. */ diff -r dc78785427d0 -r 3b4deb99a932 src/Pure/Tools/named_theorems.ML --- a/src/Pure/Tools/named_theorems.ML Wed Aug 13 17:17:51 2014 +0200 +++ b/src/Pure/Tools/named_theorems.ML Wed Aug 13 20:43:19 2014 +0200 @@ -65,22 +65,10 @@ val description = "declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr); val lthy' = lthy - |> Local_Theory.background_theory - (Global_Theory.add_thms_dynamic (binding, fn context => content context name) #> - Attrib.setup binding (Attrib.add_del (add name) (del name)) description #> - Context.theory_map (new_entry name)) + |> Local_Theory.background_theory (Context.theory_map (new_entry name)) |> Local_Theory.map_contexts (K (Context.proof_map (new_entry name))) - |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context => - let - val binding' = Morphism.binding phi binding; - val context' = - context |> Context.mapping - (Global_Theory.alias_fact binding' name) - (fn ctxt => - if Facts.defined (Proof_Context.facts_of ctxt) name - then Proof_Context.fact_alias binding' name ctxt - else ctxt); - in context' end); + |> Local_Theory.add_thms_dynamic (binding, fn context => content context name) + |> Attrib.local_setup binding (Attrib.add_del (add name) (del name)) description in (name, lthy') end; val _ = diff -r dc78785427d0 -r 3b4deb99a932 src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Wed Aug 13 17:17:51 2014 +0200 +++ b/src/Pure/global_theory.ML Wed Aug 13 20:43:19 2014 +0200 @@ -29,6 +29,8 @@ val add_thms: ((binding * thm) * attribute list) list -> theory -> thm list * theory val add_thm: (binding * thm) * attribute list -> theory -> thm * theory val add_thmss: ((binding * thm list) * attribute list) list -> theory -> thm list list * theory + val add_thms_dynamic': Context.generic -> binding * (Context.generic -> thm list) -> + theory -> string * theory val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory @@ -157,10 +159,14 @@ val add_thm = yield_singleton add_thms; -(* add_thms_dynamic *) +(* dynamic theorems *) -fun add_thms_dynamic (b, f) thy = thy - |> Data.map (Facts.add_dynamic (Context.Theory thy) (b, f) #> snd); +fun add_thms_dynamic' context arg thy = + let val (name, facts') = Facts.add_dynamic context arg (Data.get thy) + in (name, Data.put facts' thy) end; + +fun add_thms_dynamic arg thy = + add_thms_dynamic' (Context.Theory thy) arg thy |> snd; (* note_thmss *)