# 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>\theory/parents\ - (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;