more robust: parents are strict in Export_Theory.read_theory and thus approximate "commit" of exports;
authorwenzelm
Mon Sep 03 20:46:09 2018 +0200 (9 months ago)
changeset 689001145b25c53de
parent 68899 b15b03c13dbb
child 68901 4824cc40f42e
more robust: parents are strict in Export_Theory.read_theory and thus approximate "commit" of exports;
src/Pure/Thy/export_theory.ML
     1.1 --- a/src/Pure/Thy/export_theory.ML	Mon Sep 03 20:04:51 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Mon Sep 03 20:46:09 2018 +0200
     1.3 @@ -49,17 +49,10 @@
     1.4  
     1.5  val _ = setup_presentation (fn {adjust_pos, ...} => fn thy =>
     1.6    let
     1.7 +    val parents = Theory.parents_of thy;
     1.8      val rep_tsig = Type.rep_tsig (Sign.tsig_of thy);
     1.9  
    1.10  
    1.11 -    (* parents *)
    1.12 -
    1.13 -    val parents = Theory.parents_of thy;
    1.14 -    val _ =
    1.15 -      export_body thy "parents"
    1.16 -        (XML.Encode.string (cat_lines (map Context.theory_long_name parents)));
    1.17 -
    1.18 -
    1.19      (* entities *)
    1.20  
    1.21      fun entity_markup space name =
    1.22 @@ -214,6 +207,13 @@
    1.23        export_entities "locales" (fn _ => SOME o encode_locale) Locale.locale_space
    1.24          (Locale.dest_locales thy);
    1.25  
    1.26 +
    1.27 +    (* parents *)
    1.28 +
    1.29 +    val _ =
    1.30 +      export_body thy "parents"
    1.31 +        (XML.Encode.string (cat_lines (map Context.theory_long_name parents)));
    1.32 +
    1.33    in () end);
    1.34  
    1.35  end;