# 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 *)