read theory content from session database;
authorwenzelm
Thu May 17 14:50:48 2018 +0200 (6 months ago)
changeset 68203cda4f24331d5
parent 68202 a99180ad3441
child 68204 a554da2811f2
read theory content from session database;
src/Pure/Thy/export_theory.scala
     1.1 --- a/src/Pure/Thy/export_theory.scala	Thu May 17 14:40:58 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.scala	Thu May 17 14:50:48 2018 +0200
     1.3 @@ -9,6 +9,20 @@
     1.4  
     1.5  object Export_Theory
     1.6  {
     1.7 +  /** theory content **/
     1.8 +
     1.9 +  sealed case class Theory(types: List[Type], consts: List[Const])
    1.10 +
    1.11 +  def read_theory(db: SQL.Database, session_name: String, theory_name: String,
    1.12 +    types: Boolean = true,
    1.13 +    consts: Boolean = true): Theory =
    1.14 +  {
    1.15 +    Theory(
    1.16 +      if (types) read_types(db, session_name, theory_name) else Nil,
    1.17 +      if (consts) read_consts(db, session_name, theory_name) else Nil)
    1.18 +  }
    1.19 +
    1.20 +
    1.21    /* entities */
    1.22  
    1.23    sealed case class Entity(name: String, serial: Long, pos: Position.T)
    1.24 @@ -30,21 +44,32 @@
    1.25      }
    1.26    }
    1.27  
    1.28 +  def read_entities[A](db: SQL.Database, session_name: String, theory_name: String,
    1.29 +    export_name: String, decode: XML.Tree => A): List[A] =
    1.30 +  {
    1.31 +    Export.read_entry(db, session_name, theory_name, "theory/" + export_name) match {
    1.32 +      case Some(entry) => entry.uncompressed_yxml().map(decode(_))
    1.33 +      case None => Nil
    1.34 +    }
    1.35 +  }
    1.36 +
    1.37  
    1.38    /* types */
    1.39  
    1.40    sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ])
    1.41  
    1.42 -  def decode_type(tree: XML.Tree): Type =
    1.43 -  {
    1.44 -    val (entity, body) = decode_entity(tree)
    1.45 -    val (args, abbrev) =
    1.46 -    {
    1.47 -      import XML.Decode._
    1.48 -      pair(list(string), option(Term_XML.Decode.typ))(body)
    1.49 -    }
    1.50 -    Type(entity, args, abbrev)
    1.51 -  }
    1.52 +  def read_types(db: SQL.Database, session_name: String, theory_name: String): List[Type] =
    1.53 +    read_entities(db, session_name, theory_name, "types",
    1.54 +      (tree: XML.Tree) =>
    1.55 +        {
    1.56 +          val (entity, body) = decode_entity(tree)
    1.57 +          val (args, abbrev) =
    1.58 +          {
    1.59 +            import XML.Decode._
    1.60 +            pair(list(string), option(Term_XML.Decode.typ))(body)
    1.61 +          }
    1.62 +          Type(entity, args, abbrev)
    1.63 +        })
    1.64  
    1.65  
    1.66    /* consts */
    1.67 @@ -52,14 +77,16 @@
    1.68    sealed case class Const(
    1.69      entity: Entity, typargs: List[String], typ: Term.Typ, abbrev: Option[Term.Term])
    1.70  
    1.71 -  def decode_const(tree: XML.Tree): Const =
    1.72 -  {
    1.73 -    val (entity, body) = decode_entity(tree)
    1.74 -    val (args, typ, abbrev) =
    1.75 -    {
    1.76 -      import XML.Decode._
    1.77 -      triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
    1.78 -    }
    1.79 -    Const(entity, args, typ, abbrev)
    1.80 -  }
    1.81 +  def read_consts(db: SQL.Database, session_name: String, theory_name: String): List[Const] =
    1.82 +    read_entities(db, session_name, theory_name, "consts",
    1.83 +      (tree: XML.Tree) =>
    1.84 +        {
    1.85 +          val (entity, body) = decode_entity(tree)
    1.86 +          val (args, typ, abbrev) =
    1.87 +          {
    1.88 +            import XML.Decode._
    1.89 +            triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
    1.90 +          }
    1.91 +          Const(entity, args, typ, abbrev)
    1.92 +        })
    1.93  }