--- /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)
+ }
+}