# HG changeset patch
# User wenzelm
# Date 1538303174 -7200
# Node ID 06017b2c4552749e2ce8642879ccfb57e7e21927
# Parent  2859dcdbc849047ecd84e0fc39b273830e7f9c9a
suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);

diff -r 2859dcdbc849 -r 06017b2c4552 src/Pure/Isar/experiment.ML
--- a/src/Pure/Isar/experiment.ML	Sun Sep 30 11:58:59 2018 +0200
+++ b/src/Pure/Isar/experiment.ML	Sun Sep 30 12:26:14 2018 +0200
@@ -6,6 +6,7 @@
 
 signature EXPERIMENT =
 sig
+  val is_experiment: theory -> string -> bool
   val experiment: Element.context_i list -> theory -> Binding.scope * local_theory
   val experiment_cmd: Element.context list -> theory -> Binding.scope * local_theory
 end;
@@ -13,10 +14,23 @@
 structure Experiment: EXPERIMENT =
 struct
 
+structure Data = Theory_Data
+(
+  type T = Symtab.set;
+  val empty = Symtab.empty;
+  val extend = I;
+  val merge = Symtab.merge (K true);
+);
+
+fun is_experiment thy name = Symtab.defined (Data.get thy) name;
+
 fun gen_experiment add_locale elems thy =
   let
     val experiment_name = Binding.name ("experiment" ^ serial_string ()) |> Binding.concealed;
-    val (_, lthy) = thy |> add_locale experiment_name Binding.empty ([], []) elems;
+    val lthy =
+      thy
+      |> add_locale experiment_name Binding.empty ([], []) elems
+      |-> (Local_Theory.background_theory o Data.map o Symtab.insert_set);
     val (scope, naming) =
       Name_Space.new_scope (Proof_Context.naming_of (Local_Theory.target_of lthy));
     val naming' = naming |> Name_Space.private_scope scope;
diff -r 2859dcdbc849 -r 06017b2c4552 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Sun Sep 30 11:58:59 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML	Sun Sep 30 12:26:14 2018 +0200
@@ -101,7 +101,7 @@
   (fold_types o fold_atyps) (fn TFree (a, S) => is_free used a ? insert (op =) (a, S) | _ => I);
 
 
-(* locale content *)
+(* locales content *)
 
 fun locale_content thy loc =
   let
@@ -127,23 +127,31 @@
     val typargs = rev (fold Term.add_tfrees (map (Free o #1) args @ axioms) []);
   in {typargs = typargs, args = args, axioms = axioms} end;
 
-fun locale_dependency_subst thy (dep: Locale.locale_dependency) =
-  let
-    val (type_params, params) = Locale.parameters_of thy (#source dep);
-    val typargs = fold (Term.add_tfreesT o #2 o #1) params type_params;
-    val substT =
-      typargs |> map_filter (fn v =>
-        let
-          val T = TFree v;
-          val T' = Morphism.typ (#morphism dep) T;
-        in if T = T' then NONE else SOME (v, T') end);
-    val subst =
-      params |> map_filter (fn (v, _) =>
-        let
-          val t = Free v;
-          val t' = Morphism.term (#morphism dep) t;
-        in if t aconv t' then NONE else SOME (v, t') end);
-  in (substT, subst) end;
+fun get_locales thy =
+  Locale.get_locales thy |> map_filter (fn loc =>
+    if Experiment.is_experiment thy loc then NONE else SOME (loc, ()));
+
+fun get_dependencies prev_thys thy =
+  Locale.dest_dependencies prev_thys thy |> map_filter (fn dep =>
+    if Experiment.is_experiment thy (#source dep) orelse
+      Experiment.is_experiment thy (#target dep) then NONE
+    else
+      let
+        val (type_params, params) = Locale.parameters_of thy (#source dep);
+        val typargs = fold (Term.add_tfreesT o #2 o #1) params type_params;
+        val substT =
+          typargs |> map_filter (fn v =>
+            let
+              val T = TFree v;
+              val T' = Morphism.typ (#morphism dep) T;
+            in if T = T' then NONE else SOME (v, T') end);
+        val subst =
+          params |> map_filter (fn (v, _) =>
+            let
+              val t = Free v;
+              val t' = Morphism.term (#morphism dep) t;
+            in if t aconv t' then NONE else SOME (v, t') end);
+      in SOME (dep, (substT, subst)) end);
 
 
 (* general setup *)
@@ -330,14 +338,13 @@
 
     val _ =
       export_entities "locales" (fn loc => fn () => SOME (export_locale loc))
-        Locale.locale_space
-        (map (rpair ()) (Locale.get_locales thy));
+        Locale.locale_space (get_locales thy);
 
 
     (* locale dependencies *)
 
-    fun encode_locale_dependency (dep: Locale.locale_dependency) =
-      (#source dep, (#target dep, (#prefix dep, locale_dependency_subst thy dep))) |>
+    fun encode_locale_dependency (dep: Locale.locale_dependency, subst) =
+      (#source dep, (#target dep, (#prefix dep, subst))) |>
         let
           open XML.Encode Term_XML.Encode;
           val encode_subst =
@@ -345,15 +352,16 @@
         in pair string (pair string (pair (list (pair string bool)) encode_subst)) end;
 
     val _ =
-      (case Locale.dest_dependencies parents thy of
+      (case get_dependencies parents thy of
         [] => ()
       | deps =>
           deps |> map_index (fn (i, dep) =>
             let
               val xname = string_of_int (i + 1);
               val name = Long_Name.implode [Context.theory_name thy, xname];
+              val markup = make_entity_markup name xname (#pos (#1 dep)) (#serial (#1 dep));
               val body = encode_locale_dependency dep;
-            in XML.Elem (make_entity_markup name xname (#pos dep) (#serial dep), body) end)
+            in XML.Elem (markup, body) end)
           |> export_body thy "locale_dependencies");