clarified encoding;
authorwenzelm
Sun May 20 15:37:16 2018 +0200 (14 months ago)
changeset 682310004e7a9fa10
parent 68230 9bee37c2ac2b
child 68232 4b93573ac5b4
clarified encoding;
src/Pure/Thy/export_theory.ML
src/Pure/Thy/export_theory.scala
     1.1 --- a/src/Pure/Thy/export_theory.ML	Sun May 20 15:28:59 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Sun May 20 15:37:16 2018 +0200
     1.3 @@ -32,8 +32,7 @@
     1.4      val parents = Theory.parents_of thy;
     1.5      val _ =
     1.6        export_body thy "parents"
     1.7 -        let open XML.Encode
     1.8 -        in list string (map Context.theory_long_name parents) end;
     1.9 +        (XML.Encode.string (cat_lines (map Context.theory_long_name parents)));
    1.10  
    1.11  
    1.12      (* entities *)
     2.1 --- a/src/Pure/Thy/export_theory.scala	Sun May 20 15:28:59 2018 +0200
     2.2 +++ b/src/Pure/Thy/export_theory.scala	Sun May 20 15:37:16 2018 +0200
     2.3 @@ -68,9 +68,7 @@
     2.4    {
     2.5      val parents =
     2.6        Export.read_entry(db, session_name, theory_name, "theory/parents") match {
     2.7 -        case Some(entry) =>
     2.8 -          import XML.Decode._
     2.9 -          list(string)(entry.uncompressed_yxml())
    2.10 +        case Some(entry) => split_lines(entry.uncompressed().text)
    2.11          case None =>
    2.12            error("Missing theory export in session " + quote(session_name) + ": " +
    2.13              quote(theory_name))