more robust: parents are strict in Export_Theory.read_theory and thus approximate "commit" of exports;
--- a/src/Pure/Thy/export_theory.ML Mon Sep 03 20:04:51 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML Mon Sep 03 20:46:09 2018 +0200
@@ -49,17 +49,10 @@
val _ = setup_presentation (fn {adjust_pos, ...} => fn thy =>
let
+ val parents = Theory.parents_of thy;
val rep_tsig = Type.rep_tsig (Sign.tsig_of thy);
- (* parents *)
-
- val parents = Theory.parents_of thy;
- val _ =
- export_body thy "parents"
- (XML.Encode.string (cat_lines (map Context.theory_long_name parents)));
-
-
(* entities *)
fun entity_markup space name =
@@ -214,6 +207,13 @@
export_entities "locales" (fn _ => SOME o encode_locale) Locale.locale_space
(Locale.dest_locales thy);
+
+ (* parents *)
+
+ val _ =
+ export_body thy "parents"
+ (XML.Encode.string (cat_lines (map Context.theory_long_name parents)));
+
in () end);
end;