src/Pure/General/xml_data.scala

simplified XML_Data;

/*  Title:      Pure/General/xml_data.scala
    Author:     Makarius

XML as basic data representation language.
*/

package isabelle



object XML_Data
{
  /** make **/

  object Make
  {
    /* basic values */

    private def long_atom(i: Long): String = i.toString

    private def int_atom(i: Int): String = i.toString

    private def bool_atom(b: Boolean): String = if (b) "1" else "0"

    private def unit_atom(u: Unit) = ""


    /* structural nodes */

    private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)

    private def tagged(tag: Int, ts: XML.Body): XML.Tree =
      XML.Elem(Markup(int_atom(tag), Nil), ts)


    /* representation of standard types */

    def properties(props: List[(String, String)]): XML.Body =
      List(XML.Elem(Markup(":", props), Nil))

    def string(s: String): XML.Body = if (s.isEmpty) Nil else List(XML.Text(s))

    def long(i: Long): XML.Body = string(long_atom(i))

    def int(i: Int): XML.Body = string(int_atom(i))

    def bool(b: Boolean): XML.Body = string(bool_atom(b))

    def unit(u: Unit): XML.Body = string(unit_atom(u))

    def pair[A, B](f: A => XML.Body, g: B => XML.Body)(p: (A, B)): XML.Body =
      List(node(f(p._1)), node(g(p._2)))

    def triple[A, B, C](f: A => XML.Body, g: B => XML.Body, h: C => XML.Body)
        (p: (A, B, C)): XML.Body =
      List(node(f(p._1)), node(g(p._2)), node(h(p._3)))

    def list[A](f: A => XML.Body)(xs: List[A]): XML.Body =
      xs.map((x: A) => node(f(x)))

    def option[A](f: A => XML.Body)(opt: Option[A]): XML.Body =
      opt match {
        case None => Nil
        case Some(x) => List(node(f(x)))
      }

    def variant[A](fs: List[PartialFunction[A, XML.Body]])(x: A): XML.Body =
    {
      val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
      List(tagged(tag, f(x)))
    }
  }



  /** dest **/

  class XML_Atom(s: String) extends Exception(s)
  class XML_Body(body: XML.Body) extends Exception

  object Dest
  {
     /* basic values */

    private def long_atom(s: String): Long =
      try { java.lang.Long.parseLong(s) }
      catch { case e: NumberFormatException => throw new XML_Atom(s) }

    private def int_atom(s: String): Int =
      try { Integer.parseInt(s) }
      catch { case e: NumberFormatException => throw new XML_Atom(s) }

    private def bool_atom(s: String): Boolean =
      if (s == "1") true
      else if (s == "0") false
      else throw new XML_Atom(s)

    private def unit_atom(s: String): Unit =
      if (s == "") () else throw new XML_Atom(s)


    /* structural nodes */

    private def node(t: XML.Tree): XML.Body =
      t match {
        case XML.Elem(Markup(":", Nil), ts) => ts
        case _ => throw new XML_Body(List(t))
      }

    private def tagged(t: XML.Tree): (Int, XML.Body) =
      t match {
        case XML.Elem(Markup(s, Nil), ts) => (int_atom(s), ts)
        case _ => throw new XML_Body(List(t))
      }


    /* representation of standard types */

    def properties(ts: XML.Body): List[(String, String)] =
      ts match {
        case List(XML.Elem(Markup(":", props), Nil)) => props
        case _ => throw new XML_Body(ts)
      }

    def string(ts: XML.Body): String =
      ts match {
        case Nil => ""
        case List(XML.Text(s)) => s
        case _ => throw new XML_Body(ts)
      }

    def long(ts: XML.Body): Long = long_atom(string(ts))

    def int(ts: XML.Body): Int = int_atom(string(ts))

    def bool(ts: XML.Body) = bool_atom(string(ts))

    def unit(ts: XML.Body): Unit = unit_atom(string(ts))

    def pair[A, B](f: XML.Body => A, g: XML.Body => B)(ts: XML.Body): (A, B) =
      ts match {
        case List(t1, t2) => (f(node(t1)), g(node(t2)))
        case _ => throw new XML_Body(ts)
      }

    def triple[A, B, C](f: XML.Body => A, g: XML.Body => B, h: XML.Body => C)
        (ts: XML.Body): (A, B, C) =
      ts match {
        case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
        case _ => throw new XML_Body(ts)
      }

    def list[A](f: XML.Body => A)(ts: XML.Body): List[A] =
      ts.map((t: XML.Tree) => f(node(t)))

    def option[A](f: XML.Body => A)(ts: XML.Body): Option[A] =
      ts match {
        case Nil => None
        case List(t) => Some(f(node(t)))
        case _ => throw new XML_Body(ts)
      }

    def variant[A](fs: List[XML.Body => A])(ts: XML.Body): A =
      ts match {
        case List(t) =>
          val (tag, ts) = tagged(t)
          fs(tag)(ts)
        case _ => throw new XML_Body(ts)
      }
  }
}