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