src/Pure/Thy/export_theory.scala
changeset 68206 dedf1a70d1fa
parent 68203 cda4f24331d5
child 68208 d9f2cf4fc002
     1.1 --- a/src/Pure/Thy/export_theory.scala	Thu May 17 16:42:13 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.scala	Thu May 17 17:29:17 2018 +0200
     1.3 @@ -9,15 +9,73 @@
     1.4  
     1.5  object Export_Theory
     1.6  {
     1.7 +  /** session content **/
     1.8 +
     1.9 +  sealed case class Session(name: String, theory_graph: Graph[String, Theory])
    1.10 +  {
    1.11 +    override def toString: String = name
    1.12 +
    1.13 +    def theory(theory_name: String): Theory =
    1.14 +      if (theory_graph.defined(theory_name)) theory_graph.get_node(theory_name)
    1.15 +      else error("Bad theory " + quote(theory_name))
    1.16 +
    1.17 +    def theories: List[Theory] =
    1.18 +      theory_graph.topological_order.map(theory_graph.get_node(_))
    1.19 +  }
    1.20 +
    1.21 +  def read_session(session_name: String,
    1.22 +    system_mode: Boolean = false,
    1.23 +    types: Boolean = true,
    1.24 +    consts: Boolean = true): Session =
    1.25 +  {
    1.26 +    val store = Sessions.store(system_mode)
    1.27 +
    1.28 +    val thys =
    1.29 +      using(SQLite.open_database(store.the_database(session_name)))(db =>
    1.30 +      {
    1.31 +        db.transaction {
    1.32 +          Export.read_theory_names(db, session_name).iterator.map(_._1).toSet.iterator.
    1.33 +            map((theory_name: String) =>
    1.34 +              read_theory(db, session_name, theory_name, types = types, consts = consts)).toList
    1.35 +        }
    1.36 +      })
    1.37 +
    1.38 +    val graph0 =
    1.39 +      (Graph.string[Theory] /: thys) { case (g, thy) => g.new_node(thy.name, thy) }
    1.40 +    val graph1 =
    1.41 +      (graph0 /: thys) { case (g0, thy) =>
    1.42 +        (g0 /: thy.parents) { case (g1, parent) =>
    1.43 +          g1.default_node(parent, empty_theory(parent)).add_edge_acyclic(parent, thy.name) } }
    1.44 +
    1.45 +    Session(session_name, graph1)
    1.46 +  }
    1.47 +
    1.48 +
    1.49 +
    1.50    /** theory content **/
    1.51  
    1.52 -  sealed case class Theory(types: List[Type], consts: List[Const])
    1.53 +  sealed case class Theory(
    1.54 +    name: String, parents: List[String], types: List[Type], consts: List[Const])
    1.55 +  {
    1.56 +    override def toString: String = name
    1.57 +  }
    1.58 +
    1.59 +  def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil)
    1.60  
    1.61    def read_theory(db: SQL.Database, session_name: String, theory_name: String,
    1.62      types: Boolean = true,
    1.63      consts: Boolean = true): Theory =
    1.64    {
    1.65 -    Theory(
    1.66 +    val parents =
    1.67 +      Export.read_entry(db, session_name, theory_name, "theory/parents") match {
    1.68 +        case Some(entry) =>
    1.69 +          import XML.Decode._
    1.70 +          list(string)(entry.uncompressed_yxml())
    1.71 +        case None =>
    1.72 +          error("Missing theory export in session " + quote(session_name) + ": " +
    1.73 +            quote(theory_name))
    1.74 +      }
    1.75 +    Theory(theory_name, parents,
    1.76        if (types) read_types(db, session_name, theory_name) else Nil,
    1.77        if (consts) read_consts(db, session_name, theory_name) else Nil)
    1.78    }