--- 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)
--- 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;
--- 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;
--- 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 **)
--- 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!?
--- 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 =
--- 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()
--- 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.
*/
--- 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";
--- 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.
*/
--- 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 _ =
--- 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 *)