src/Pure/Thy/export_theory.scala

more uniform types vs. consts;

/*  Title:      Pure/Thy/export_theory.scala
    Author:     Makarius

Export foundational theory content.
*/

package isabelle


object Export_Theory
{
  /* entities */

  sealed case class Entity(name: 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 serial = Markup.Serial.unapply(props) getOrElse err()
        val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) })
        (Entity(name, serial, pos), body)
      case _ => err()
    }
  }


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


  /* consts */

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