# HG changeset patch
# User wenzelm
# Date 1526234699 -7200
# Node ID 13162bb3a6775475304e40c2440ca9bf998f4b7f
# Parent  7e1daf6f2578a015d25efff70824c149561e1e5a
export foundational theory content in Scala;

diff -r 7e1daf6f2578 -r 13162bb3a677 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sun May 13 16:51:50 2018 +0200
+++ b/src/Pure/Thy/export.scala	Sun May 13 20:04:59 2018 +0200
@@ -86,6 +86,9 @@
       val (compressed, bytes) = body.join
       if (compressed) bytes.uncompress(cache = cache) else bytes
     }
+
+    def uncompressed_yxml(cache: XZ.Cache = XZ.cache()): XML.Body =
+      YXML.parse_body(UTF8.decode_permissive(uncompressed(cache = cache)))
   }
 
   def make_regex(pattern: String): Regex =
diff -r 7e1daf6f2578 -r 13162bb3a677 src/Pure/Thy/export_theory.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/export_theory.scala	Sun May 13 20:04:59 2018 +0200
@@ -0,0 +1,68 @@
+/*  Title:      Pure/Thy/export_theory.scala
+    Author:     Makarius
+
+Export foundational theory content.
+*/
+
+package isabelle
+
+
+object Export_Theory
+{
+  /* entities */
+
+  sealed case class Entity(name: String, kind: String, serial: Long, pos: Position.T)
+  {
+    override def toString: String = name
+  }
+
+  def decode_entity(tree: XML.Tree): (Entity, XML.Body) =
+  {
+    def err(): Nothing = throw new XML.XML_Body(List(tree))
+
+    tree match {
+      case XML.Elem(Markup(Markup.ENTITY, props), body) =>
+        val name = Markup.Name.unapply(props) getOrElse err()
+        val kind = Markup.Kind.unapply(props) getOrElse err()
+        val serial = Markup.Serial.unapply(props) getOrElse err()
+        val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) })
+        (Entity(name, kind, serial, pos), body)
+      case _ => err()
+    }
+  }
+
+
+  /* types */
+
+  sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ])
+  {
+    def arity: Int = args.length
+  }
+
+  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)
+  }
+
+
+  /* consts */
+
+  sealed case class Const(entity: Entity, typ: Term.Typ, abbrev: Option[Term.Term])
+
+  def decode_const(tree: XML.Tree): Const =
+  {
+    val (entity, body) = decode_entity(tree)
+    val (typ, abbrev) =
+    {
+      import XML.Decode._
+      pair(Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
+    }
+    Const(entity, typ, abbrev)
+  }
+}
diff -r 7e1daf6f2578 -r 13162bb3a677 src/Pure/build-jars
--- a/src/Pure/build-jars	Sun May 13 16:51:50 2018 +0200
+++ b/src/Pure/build-jars	Sun May 13 20:04:59 2018 +0200
@@ -128,6 +128,7 @@
   System/tty_loop.scala
   Thy/bibtex.scala
   Thy/export.scala
+  Thy/export_theory.scala
   Thy/html.scala
   Thy/latex.scala
   Thy/present.scala