# HG changeset patch
# User wenzelm
# Date 1526561448 -7200
# Node ID cda4f24331d58620bb4acd5b19e631cca79a1227
# Parent  a99180ad34410f5e63036b6800f8691d067165ff
read theory content from session database;

diff -r a99180ad3441 -r cda4f24331d5 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Thu May 17 14:40:58 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala	Thu May 17 14:50:48 2018 +0200
@@ -9,6 +9,20 @@
 
 object Export_Theory
 {
+  /** theory content **/
+
+  sealed case class Theory(types: List[Type], consts: List[Const])
+
+  def read_theory(db: SQL.Database, session_name: String, theory_name: String,
+    types: Boolean = true,
+    consts: Boolean = true): Theory =
+  {
+    Theory(
+      if (types) read_types(db, session_name, theory_name) else Nil,
+      if (consts) read_consts(db, session_name, theory_name) else Nil)
+  }
+
+
   /* entities */
 
   sealed case class Entity(name: String, serial: Long, pos: Position.T)
@@ -30,21 +44,32 @@
     }
   }
 
+  def read_entities[A](db: SQL.Database, session_name: String, theory_name: String,
+    export_name: String, decode: XML.Tree => A): List[A] =
+  {
+    Export.read_entry(db, session_name, theory_name, "theory/" + export_name) match {
+      case Some(entry) => entry.uncompressed_yxml().map(decode(_))
+      case None => Nil
+    }
+  }
+
 
   /* types */
 
   sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ])
 
-  def decode_type(tree: XML.Tree): Type =
-  {
-    val (entity, body) = decode_entity(tree)
-    val (args, abbrev) =
-    {
-      import XML.Decode._
-      pair(list(string), option(Term_XML.Decode.typ))(body)
-    }
-    Type(entity, args, abbrev)
-  }
+  def read_types(db: SQL.Database, session_name: String, theory_name: String): List[Type] =
+    read_entities(db, session_name, theory_name, "types",
+      (tree: XML.Tree) =>
+        {
+          val (entity, body) = decode_entity(tree)
+          val (args, abbrev) =
+          {
+            import XML.Decode._
+            pair(list(string), option(Term_XML.Decode.typ))(body)
+          }
+          Type(entity, args, abbrev)
+        })
 
 
   /* consts */
@@ -52,14 +77,16 @@
   sealed case class Const(
     entity: Entity, typargs: List[String], typ: Term.Typ, abbrev: Option[Term.Term])
 
-  def decode_const(tree: XML.Tree): Const =
-  {
-    val (entity, body) = decode_entity(tree)
-    val (args, typ, abbrev) =
-    {
-      import XML.Decode._
-      triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
-    }
-    Const(entity, args, typ, abbrev)
-  }
+  def read_consts(db: SQL.Database, session_name: String, theory_name: String): List[Const] =
+    read_entities(db, session_name, theory_name, "consts",
+      (tree: XML.Tree) =>
+        {
+          val (entity, body) = decode_entity(tree)
+          val (args, typ, abbrev) =
+          {
+            import XML.Decode._
+            triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
+          }
+          Const(entity, args, typ, abbrev)
+        })
 }