# HG changeset patch
# User wenzelm
# Date 1659701142 -7200
# Node ID 8cf14d4ebec47b8ebc60bbd3529ab8b23370e234
# Parent  985c3a64748c2e892bf2a98a60a1996ed1567c9f
more uniform exports: proper encoding of empty parents for Pure;

diff -r 985c3a64748c -r 8cf14d4ebec4 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Fri Aug 05 13:43:14 2022 +0200
+++ b/src/Pure/Thy/export_theory.ML	Fri Aug 05 14:05:42 2022 +0200
@@ -156,7 +156,7 @@
     val parents = Theory.parents_of thy;
     val _ =
       Export.export thy \<^path_binding>\<open>theory/parents\<close>
-        (XML.Encode.string (cat_lines (map Context.theory_long_name parents)));
+        (XML.Encode.string (terminate_lines (map Context.theory_long_name parents)));
 
 
     (* spec rules *)
diff -r 985c3a64748c -r 8cf14d4ebec4 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Fri Aug 05 13:43:14 2022 +0200
+++ b/src/Pure/Thy/export_theory.scala	Fri Aug 05 14:05:42 2022 +0200
@@ -107,13 +107,9 @@
         (for ((k, xs) <- others.iterator) yield cache.string(k) -> xs.map(_.cache(cache))).toMap)
   }
 
-  def read_theory_parents(provider: Export.Provider, theory_name: String): Option[List[String]] = {
-    if (theory_name == Thy_Header.PURE) Some(Nil)
-    else {
-      provider.focus(theory_name)(Export.THEORY_PREFIX + "parents")
-        .map(entry => split_lines(entry.uncompressed.text))
-    }
-  }
+  def read_theory_parents(provider: Export.Provider, theory_name: String): Option[List[String]] =
+    provider.focus(theory_name)(Export.THEORY_PREFIX + "parents")
+      .map(entry => Library.trim_split_lines(entry.uncompressed.text))
 
   def no_theory: Theory =
     Theory("", Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Map.empty)
diff -r 985c3a64748c -r 8cf14d4ebec4 src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Aug 05 13:43:14 2022 +0200
+++ b/src/Pure/library.ML	Fri Aug 05 14:05:42 2022 +0200
@@ -145,6 +145,7 @@
   val commas: string list -> string
   val commas_quote: string list -> string
   val cat_lines: string list -> string
+  val terminate_lines: string list -> string
   val space_explode: string -> string -> string list
   val split_lines: string -> string list
   val plain_words: string -> string
@@ -748,6 +749,8 @@
 
 val cat_lines = space_implode "\n";
 
+fun terminate_lines lines = cat_lines lines ^ "\n";
+
 (*space_explode "." "h.e..l.lo" = ["h", "e", "", "l", "lo"]*)
 fun space_explode _ "" = []
   | space_explode sep s = String.fields (fn c => str c = sep) s;