# HG changeset patch # User wenzelm # Date 1526823436 -7200 # Node ID 0004e7a9fa10d27c2013496550e1ad3a2260bec0 # Parent 9bee37c2ac2b2e32df287e32fe4cee13156768f3 clarified encoding; diff -r 9bee37c2ac2b -r 0004e7a9fa10 src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML Sun May 20 15:28:59 2018 +0200 +++ b/src/Pure/Thy/export_theory.ML Sun May 20 15:37:16 2018 +0200 @@ -32,8 +32,7 @@ val parents = Theory.parents_of thy; val _ = export_body thy "parents" - let open XML.Encode - in list string (map Context.theory_long_name parents) end; + (XML.Encode.string (cat_lines (map Context.theory_long_name parents))); (* entities *) diff -r 9bee37c2ac2b -r 0004e7a9fa10 src/Pure/Thy/export_theory.scala --- a/src/Pure/Thy/export_theory.scala Sun May 20 15:28:59 2018 +0200 +++ b/src/Pure/Thy/export_theory.scala Sun May 20 15:37:16 2018 +0200 @@ -68,9 +68,7 @@ { val parents = Export.read_entry(db, session_name, theory_name, "theory/parents") match { - case Some(entry) => - import XML.Decode._ - list(string)(entry.uncompressed_yxml()) + case Some(entry) => split_lines(entry.uncompressed().text) case None => error("Missing theory export in session " + quote(session_name) + ": " + quote(theory_name))