src/Pure/Thy/export_theory.scala
author wenzelm
Sun May 13 20:24:33 2018 +0200 (14 months ago)
changeset 68172 0f14cf9c632f
parent 68171 13162bb3a677
child 68173 7ed88a534bb6
permissions -rw-r--r--
more concise information;
wenzelm@68171
     1
/*  Title:      Pure/Thy/export_theory.scala
wenzelm@68171
     2
    Author:     Makarius
wenzelm@68171
     3
wenzelm@68171
     4
Export foundational theory content.
wenzelm@68171
     5
*/
wenzelm@68171
     6
wenzelm@68171
     7
package isabelle
wenzelm@68171
     8
wenzelm@68171
     9
wenzelm@68171
    10
object Export_Theory
wenzelm@68171
    11
{
wenzelm@68171
    12
  /* entities */
wenzelm@68171
    13
wenzelm@68172
    14
  sealed case class Entity(name: String, serial: Long, pos: Position.T)
wenzelm@68171
    15
  {
wenzelm@68171
    16
    override def toString: String = name
wenzelm@68171
    17
  }
wenzelm@68171
    18
wenzelm@68171
    19
  def decode_entity(tree: XML.Tree): (Entity, XML.Body) =
wenzelm@68171
    20
  {
wenzelm@68171
    21
    def err(): Nothing = throw new XML.XML_Body(List(tree))
wenzelm@68171
    22
wenzelm@68171
    23
    tree match {
wenzelm@68171
    24
      case XML.Elem(Markup(Markup.ENTITY, props), body) =>
wenzelm@68171
    25
        val name = Markup.Name.unapply(props) getOrElse err()
wenzelm@68171
    26
        val serial = Markup.Serial.unapply(props) getOrElse err()
wenzelm@68171
    27
        val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) })
wenzelm@68172
    28
        (Entity(name, serial, pos), body)
wenzelm@68171
    29
      case _ => err()
wenzelm@68171
    30
    }
wenzelm@68171
    31
  }
wenzelm@68171
    32
wenzelm@68171
    33
wenzelm@68171
    34
  /* types */
wenzelm@68171
    35
wenzelm@68171
    36
  sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ])
wenzelm@68171
    37
  {
wenzelm@68171
    38
    def arity: Int = args.length
wenzelm@68171
    39
  }
wenzelm@68171
    40
wenzelm@68171
    41
  def decode_type(tree: XML.Tree): Type =
wenzelm@68171
    42
  {
wenzelm@68171
    43
    val (entity, body) = decode_entity(tree)
wenzelm@68171
    44
    val (args, abbrev) =
wenzelm@68171
    45
    {
wenzelm@68171
    46
      import XML.Decode._
wenzelm@68171
    47
      pair(list(string), option(Term_XML.Decode.typ))(body)
wenzelm@68171
    48
    }
wenzelm@68171
    49
    Type(entity, args, abbrev)
wenzelm@68171
    50
  }
wenzelm@68171
    51
wenzelm@68171
    52
wenzelm@68171
    53
  /* consts */
wenzelm@68171
    54
wenzelm@68171
    55
  sealed case class Const(entity: Entity, typ: Term.Typ, abbrev: Option[Term.Term])
wenzelm@68171
    56
wenzelm@68171
    57
  def decode_const(tree: XML.Tree): Const =
wenzelm@68171
    58
  {
wenzelm@68171
    59
    val (entity, body) = decode_entity(tree)
wenzelm@68171
    60
    val (typ, abbrev) =
wenzelm@68171
    61
    {
wenzelm@68171
    62
      import XML.Decode._
wenzelm@68171
    63
      pair(Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
wenzelm@68171
    64
    }
wenzelm@68171
    65
    Const(entity, typ, abbrev)
wenzelm@68171
    66
  }
wenzelm@68171
    67
}