export foundational theory content in Scala;
authorwenzelm
Sun May 13 20:04:59 2018 +0200 (12 months ago)
changeset 6817113162bb3a677
parent 68170 7e1daf6f2578
child 68172 0f14cf9c632f
export foundational theory content in Scala;
src/Pure/Thy/export.scala
src/Pure/Thy/export_theory.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/Thy/export.scala	Sun May 13 16:51:50 2018 +0200
     1.2 +++ b/src/Pure/Thy/export.scala	Sun May 13 20:04:59 2018 +0200
     1.3 @@ -86,6 +86,9 @@
     1.4        val (compressed, bytes) = body.join
     1.5        if (compressed) bytes.uncompress(cache = cache) else bytes
     1.6      }
     1.7 +
     1.8 +    def uncompressed_yxml(cache: XZ.Cache = XZ.cache()): XML.Body =
     1.9 +      YXML.parse_body(UTF8.decode_permissive(uncompressed(cache = cache)))
    1.10    }
    1.11  
    1.12    def make_regex(pattern: String): Regex =
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/Thy/export_theory.scala	Sun May 13 20:04:59 2018 +0200
     2.3 @@ -0,0 +1,68 @@
     2.4 +/*  Title:      Pure/Thy/export_theory.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Export foundational theory content.
     2.8 +*/
     2.9 +
    2.10 +package isabelle
    2.11 +
    2.12 +
    2.13 +object Export_Theory
    2.14 +{
    2.15 +  /* entities */
    2.16 +
    2.17 +  sealed case class Entity(name: String, kind: String, serial: Long, pos: Position.T)
    2.18 +  {
    2.19 +    override def toString: String = name
    2.20 +  }
    2.21 +
    2.22 +  def decode_entity(tree: XML.Tree): (Entity, XML.Body) =
    2.23 +  {
    2.24 +    def err(): Nothing = throw new XML.XML_Body(List(tree))
    2.25 +
    2.26 +    tree match {
    2.27 +      case XML.Elem(Markup(Markup.ENTITY, props), body) =>
    2.28 +        val name = Markup.Name.unapply(props) getOrElse err()
    2.29 +        val kind = Markup.Kind.unapply(props) getOrElse err()
    2.30 +        val serial = Markup.Serial.unapply(props) getOrElse err()
    2.31 +        val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) })
    2.32 +        (Entity(name, kind, serial, pos), body)
    2.33 +      case _ => err()
    2.34 +    }
    2.35 +  }
    2.36 +
    2.37 +
    2.38 +  /* types */
    2.39 +
    2.40 +  sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ])
    2.41 +  {
    2.42 +    def arity: Int = args.length
    2.43 +  }
    2.44 +
    2.45 +  def decode_type(tree: XML.Tree): Type =
    2.46 +  {
    2.47 +    val (entity, body) = decode_entity(tree)
    2.48 +    val (args, abbrev) =
    2.49 +    {
    2.50 +      import XML.Decode._
    2.51 +      pair(list(string), option(Term_XML.Decode.typ))(body)
    2.52 +    }
    2.53 +    Type(entity, args, abbrev)
    2.54 +  }
    2.55 +
    2.56 +
    2.57 +  /* consts */
    2.58 +
    2.59 +  sealed case class Const(entity: Entity, typ: Term.Typ, abbrev: Option[Term.Term])
    2.60 +
    2.61 +  def decode_const(tree: XML.Tree): Const =
    2.62 +  {
    2.63 +    val (entity, body) = decode_entity(tree)
    2.64 +    val (typ, abbrev) =
    2.65 +    {
    2.66 +      import XML.Decode._
    2.67 +      pair(Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
    2.68 +    }
    2.69 +    Const(entity, typ, abbrev)
    2.70 +  }
    2.71 +}
     3.1 --- a/src/Pure/build-jars	Sun May 13 16:51:50 2018 +0200
     3.2 +++ b/src/Pure/build-jars	Sun May 13 20:04:59 2018 +0200
     3.3 @@ -128,6 +128,7 @@
     3.4    System/tty_loop.scala
     3.5    Thy/bibtex.scala
     3.6    Thy/export.scala
     3.7 +  Thy/export_theory.scala
     3.8    Thy/html.scala
     3.9    Thy/latex.scala
    3.10    Thy/present.scala