# HG changeset patch
# User wenzelm
# Date 1536000369 -7200
# Node ID 1145b25c53de5259dc012045dd6bba71ac5d0c46
# Parent  b15b03c13dbb66a39919880a3a319ec3b2375231
more robust: parents are strict in Export_Theory.read_theory and thus approximate "commit" of exports;

diff -r b15b03c13dbb -r 1145b25c53de src/Pure/Thy/export_theory.ML
--- 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;