more robust: parents are strict in Export_Theory.read_theory and thus approximate "commit" of exports;
authorwenzelm
Mon, 03 Sep 2018 20:46:09 +0200
changeset 68900 1145b25c53de
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
--- 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;