src/Pure/Thy/export_theory.scala
changeset 68231 0004e7a9fa10
parent 68222 3c1a716e7f59
child 68232 4b93573ac5b4
equal deleted inserted replaced
68230:9bee37c2ac2b 68231:0004e7a9fa10
    66     consts: Boolean = true,
    66     consts: Boolean = true,
    67     axioms: Boolean = true): Theory =
    67     axioms: Boolean = true): Theory =
    68   {
    68   {
    69     val parents =
    69     val parents =
    70       Export.read_entry(db, session_name, theory_name, "theory/parents") match {
    70       Export.read_entry(db, session_name, theory_name, "theory/parents") match {
    71         case Some(entry) =>
    71         case Some(entry) => split_lines(entry.uncompressed().text)
    72           import XML.Decode._
       
    73           list(string)(entry.uncompressed_yxml())
       
    74         case None =>
    72         case None =>
    75           error("Missing theory export in session " + quote(session_name) + ": " +
    73           error("Missing theory export in session " + quote(session_name) + ": " +
    76             quote(theory_name))
    74             quote(theory_name))
    77       }
    75       }
    78     Theory(theory_name, parents,
    76     Theory(theory_name, parents,