export more theory and session structure;
authorwenzelm
Thu May 17 17:29:17 2018 +0200 (3 months ago)
changeset 68206dedf1a70d1fa
parent 68205 9a8949f71fd4
child 68207 1463c4996fb2
export more theory and session structure;
src/Pure/Thy/export_theory.ML
src/Pure/Thy/export_theory.scala
     1.1 --- a/src/Pure/Thy/export_theory.ML	Thu May 17 16:42:13 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Thu May 17 17:29:17 2018 +0200
     1.3 @@ -27,6 +27,15 @@
     1.4  
     1.5  val _ = setup_presentation (fn {adjust_pos, ...} => fn thy =>
     1.6    let
     1.7 +    (* parents *)
     1.8 +
     1.9 +    val parents = Theory.parents_of thy;
    1.10 +    val _ =
    1.11 +      export_body thy "parents"
    1.12 +        let open XML.Encode
    1.13 +        in list string (map Context.theory_long_name parents) end;
    1.14 +
    1.15 +
    1.16      (* entities *)
    1.17  
    1.18      fun entity_markup space name =
    1.19 @@ -40,7 +49,7 @@
    1.20      fun export_entities export_name export get_space decls =
    1.21        let val elems =
    1.22          let
    1.23 -          val parent_spaces = map get_space (Theory.parents_of thy);
    1.24 +          val parent_spaces = map get_space parents;
    1.25            val space = get_space thy;
    1.26          in
    1.27            (decls, []) |-> fold (fn (name, decl) =>
     2.1 --- a/src/Pure/Thy/export_theory.scala	Thu May 17 16:42:13 2018 +0200
     2.2 +++ b/src/Pure/Thy/export_theory.scala	Thu May 17 17:29:17 2018 +0200
     2.3 @@ -9,15 +9,73 @@
     2.4  
     2.5  object Export_Theory
     2.6  {
     2.7 +  /** session content **/
     2.8 +
     2.9 +  sealed case class Session(name: String, theory_graph: Graph[String, Theory])
    2.10 +  {
    2.11 +    override def toString: String = name
    2.12 +
    2.13 +    def theory(theory_name: String): Theory =
    2.14 +      if (theory_graph.defined(theory_name)) theory_graph.get_node(theory_name)
    2.15 +      else error("Bad theory " + quote(theory_name))
    2.16 +
    2.17 +    def theories: List[Theory] =
    2.18 +      theory_graph.topological_order.map(theory_graph.get_node(_))
    2.19 +  }
    2.20 +
    2.21 +  def read_session(session_name: String,
    2.22 +    system_mode: Boolean = false,
    2.23 +    types: Boolean = true,
    2.24 +    consts: Boolean = true): Session =
    2.25 +  {
    2.26 +    val store = Sessions.store(system_mode)
    2.27 +
    2.28 +    val thys =
    2.29 +      using(SQLite.open_database(store.the_database(session_name)))(db =>
    2.30 +      {
    2.31 +        db.transaction {
    2.32 +          Export.read_theory_names(db, session_name).iterator.map(_._1).toSet.iterator.
    2.33 +            map((theory_name: String) =>
    2.34 +              read_theory(db, session_name, theory_name, types = types, consts = consts)).toList
    2.35 +        }
    2.36 +      })
    2.37 +
    2.38 +    val graph0 =
    2.39 +      (Graph.string[Theory] /: thys) { case (g, thy) => g.new_node(thy.name, thy) }
    2.40 +    val graph1 =
    2.41 +      (graph0 /: thys) { case (g0, thy) =>
    2.42 +        (g0 /: thy.parents) { case (g1, parent) =>
    2.43 +          g1.default_node(parent, empty_theory(parent)).add_edge_acyclic(parent, thy.name) } }
    2.44 +
    2.45 +    Session(session_name, graph1)
    2.46 +  }
    2.47 +
    2.48 +
    2.49 +
    2.50    /** theory content **/
    2.51  
    2.52 -  sealed case class Theory(types: List[Type], consts: List[Const])
    2.53 +  sealed case class Theory(
    2.54 +    name: String, parents: List[String], types: List[Type], consts: List[Const])
    2.55 +  {
    2.56 +    override def toString: String = name
    2.57 +  }
    2.58 +
    2.59 +  def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil)
    2.60  
    2.61    def read_theory(db: SQL.Database, session_name: String, theory_name: String,
    2.62      types: Boolean = true,
    2.63      consts: Boolean = true): Theory =
    2.64    {
    2.65 -    Theory(
    2.66 +    val parents =
    2.67 +      Export.read_entry(db, session_name, theory_name, "theory/parents") match {
    2.68 +        case Some(entry) =>
    2.69 +          import XML.Decode._
    2.70 +          list(string)(entry.uncompressed_yxml())
    2.71 +        case None =>
    2.72 +          error("Missing theory export in session " + quote(session_name) + ": " +
    2.73 +            quote(theory_name))
    2.74 +      }
    2.75 +    Theory(theory_name, parents,
    2.76        if (types) read_types(db, session_name, theory_name) else Nil,
    2.77        if (consts) read_consts(db, session_name, theory_name) else Nil)
    2.78    }