# HG changeset patch
# User wenzelm
# Date 1407929428 -7200
# Node ID 59b2572e8e93c114c52a0d361afb361abab3d5b9
# Parent  2bd92d3f92d7387721fb38f6c159aa3f2bd74b8f
load local_theory.ML before attrib.ML, with subtle change of semantics due to canonical Local_Theory.map_contexts instead of private Local_Theory.map_top;

diff -r 2bd92d3f92d7 -r 59b2572e8e93 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Wed Aug 13 12:59:27 2014 +0200
+++ b/src/Pure/Isar/expression.ML	Wed Aug 13 13:30:28 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 2bd92d3f92d7 -r 59b2572e8e93 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Wed Aug 13 12:59:27 2014 +0200
+++ b/src/Pure/Isar/generic_target.ML	Wed Aug 13 13:30:28 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 2bd92d3f92d7 -r 59b2572e8e93 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Wed Aug 13 12:59:27 2014 +0200
+++ b/src/Pure/Isar/local_theory.ML	Wed Aug 13 13:30:28 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
@@ -58,10 +65,6 @@
   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
@@ -307,17 +310,6 @@
 val const_alias = alias Sign.const_alias Proof_Context.const_alias;
 
 
-(* activation of locale fragments *)
-
-fun activate_nonbrittle dep_morph mixin export =
-  map_top (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 2bd92d3f92d7 -r 59b2572e8e93 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Aug 13 12:59:27 2014 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Aug 13 13:30:28 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 2bd92d3f92d7 -r 59b2572e8e93 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Aug 13 12:59:27 2014 +0200
+++ b/src/Pure/ROOT.ML	Wed Aug 13 13:30:28 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";