tuned signature;
authorwenzelm
Fri Jun 01 11:50:20 2018 +0200 (13 months ago)
changeset 68346b44010800a19
parent 68345 5bc1e1ac7955
child 68347 9e6e7ab77434
tuned signature;
src/Pure/Thy/export_theory.scala
     1.1 --- a/src/Pure/Thy/export_theory.scala	Fri Jun 01 11:10:22 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.scala	Fri Jun 01 11:50:20 2018 +0200
     1.3 @@ -60,6 +60,8 @@
     1.4  
     1.5    /** theory content **/
     1.6  
     1.7 +  val export_prefix: String = "theory/"
     1.8 +
     1.9    sealed case class Theory(name: String, parents: List[String],
    1.10      types: List[Type],
    1.11      consts: List[Const],
    1.12 @@ -100,7 +102,7 @@
    1.13      cache: Option[Term.Cache] = None): Theory =
    1.14    {
    1.15      val parents =
    1.16 -      Export.read_entry(db, session_name, theory_name, "theory/parents") match {
    1.17 +      Export.read_entry(db, session_name, theory_name, export_prefix + "parents") match {
    1.18          case Some(entry) => split_lines(entry.uncompressed().text)
    1.19          case None =>
    1.20            error("Missing theory export in session " + quote(session_name) + ": " +
    1.21 @@ -147,7 +149,7 @@
    1.22    def read_export[A](db: SQL.Database, session_name: String, theory_name: String,
    1.23      export_name: String, decode: XML.Body => List[A]): List[A] =
    1.24    {
    1.25 -    Export.read_entry(db, session_name, theory_name, "theory/" + export_name) match {
    1.26 +    Export.read_entry(db, session_name, theory_name, export_prefix + export_name) match {
    1.27        case Some(entry) => decode(entry.uncompressed_yxml())
    1.28        case None => Nil
    1.29      }