src/Pure/Thy/export_theory.ML
changeset 69087 06017b2c4552
parent 69086 2859dcdbc849
child 69784 24bbc4e30e5b
     1.1 --- a/src/Pure/Thy/export_theory.ML	Sun Sep 30 11:58:59 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Sun Sep 30 12:26:14 2018 +0200
     1.3 @@ -101,7 +101,7 @@
     1.4    (fold_types o fold_atyps) (fn TFree (a, S) => is_free used a ? insert (op =) (a, S) | _ => I);
     1.5  
     1.6  
     1.7 -(* locale content *)
     1.8 +(* locales content *)
     1.9  
    1.10  fun locale_content thy loc =
    1.11    let
    1.12 @@ -127,23 +127,31 @@
    1.13      val typargs = rev (fold Term.add_tfrees (map (Free o #1) args @ axioms) []);
    1.14    in {typargs = typargs, args = args, axioms = axioms} end;
    1.15  
    1.16 -fun locale_dependency_subst thy (dep: Locale.locale_dependency) =
    1.17 -  let
    1.18 -    val (type_params, params) = Locale.parameters_of thy (#source dep);
    1.19 -    val typargs = fold (Term.add_tfreesT o #2 o #1) params type_params;
    1.20 -    val substT =
    1.21 -      typargs |> map_filter (fn v =>
    1.22 -        let
    1.23 -          val T = TFree v;
    1.24 -          val T' = Morphism.typ (#morphism dep) T;
    1.25 -        in if T = T' then NONE else SOME (v, T') end);
    1.26 -    val subst =
    1.27 -      params |> map_filter (fn (v, _) =>
    1.28 -        let
    1.29 -          val t = Free v;
    1.30 -          val t' = Morphism.term (#morphism dep) t;
    1.31 -        in if t aconv t' then NONE else SOME (v, t') end);
    1.32 -  in (substT, subst) end;
    1.33 +fun get_locales thy =
    1.34 +  Locale.get_locales thy |> map_filter (fn loc =>
    1.35 +    if Experiment.is_experiment thy loc then NONE else SOME (loc, ()));
    1.36 +
    1.37 +fun get_dependencies prev_thys thy =
    1.38 +  Locale.dest_dependencies prev_thys thy |> map_filter (fn dep =>
    1.39 +    if Experiment.is_experiment thy (#source dep) orelse
    1.40 +      Experiment.is_experiment thy (#target dep) then NONE
    1.41 +    else
    1.42 +      let
    1.43 +        val (type_params, params) = Locale.parameters_of thy (#source dep);
    1.44 +        val typargs = fold (Term.add_tfreesT o #2 o #1) params type_params;
    1.45 +        val substT =
    1.46 +          typargs |> map_filter (fn v =>
    1.47 +            let
    1.48 +              val T = TFree v;
    1.49 +              val T' = Morphism.typ (#morphism dep) T;
    1.50 +            in if T = T' then NONE else SOME (v, T') end);
    1.51 +        val subst =
    1.52 +          params |> map_filter (fn (v, _) =>
    1.53 +            let
    1.54 +              val t = Free v;
    1.55 +              val t' = Morphism.term (#morphism dep) t;
    1.56 +            in if t aconv t' then NONE else SOME (v, t') end);
    1.57 +      in SOME (dep, (substT, subst)) end);
    1.58  
    1.59  
    1.60  (* general setup *)
    1.61 @@ -330,14 +338,13 @@
    1.62  
    1.63      val _ =
    1.64        export_entities "locales" (fn loc => fn () => SOME (export_locale loc))
    1.65 -        Locale.locale_space
    1.66 -        (map (rpair ()) (Locale.get_locales thy));
    1.67 +        Locale.locale_space (get_locales thy);
    1.68  
    1.69  
    1.70      (* locale dependencies *)
    1.71  
    1.72 -    fun encode_locale_dependency (dep: Locale.locale_dependency) =
    1.73 -      (#source dep, (#target dep, (#prefix dep, locale_dependency_subst thy dep))) |>
    1.74 +    fun encode_locale_dependency (dep: Locale.locale_dependency, subst) =
    1.75 +      (#source dep, (#target dep, (#prefix dep, subst))) |>
    1.76          let
    1.77            open XML.Encode Term_XML.Encode;
    1.78            val encode_subst =
    1.79 @@ -345,15 +352,16 @@
    1.80          in pair string (pair string (pair (list (pair string bool)) encode_subst)) end;
    1.81  
    1.82      val _ =
    1.83 -      (case Locale.dest_dependencies parents thy of
    1.84 +      (case get_dependencies parents thy of
    1.85          [] => ()
    1.86        | deps =>
    1.87            deps |> map_index (fn (i, dep) =>
    1.88              let
    1.89                val xname = string_of_int (i + 1);
    1.90                val name = Long_Name.implode [Context.theory_name thy, xname];
    1.91 +              val markup = make_entity_markup name xname (#pos (#1 dep)) (#serial (#1 dep));
    1.92                val body = encode_locale_dependency dep;
    1.93 -            in XML.Elem (make_entity_markup name xname (#pos dep) (#serial dep), body) end)
    1.94 +            in XML.Elem (markup, body) end)
    1.95            |> export_body thy "locale_dependencies");
    1.96  
    1.97