Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clarified encoding;
authorwenzelm
Sun, 20 May 2018 15:37:16 +0200
changeset 68231 0004e7a9fa10
parent 68230 9bee37c2ac2b
child 68232 4b93573ac5b4
clarified encoding;
src/Pure/Thy/export_theory.ML file | annotate | diff | comparison | revisions
src/Pure/Thy/export_theory.scala file | annotate | diff | comparison | revisions 
--- 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 *)
--- 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))
isabelle