src/Pure/General/xml_data.scala
changeset 43767 e0219ef7f84c
parent 43766 9545bb3cefac
child 43768 d52ab827d62b
     1.1 --- a/src/Pure/General/xml_data.scala	Tue Jul 12 16:00:05 2011 +0900
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,176 +0,0 @@
     1.4 -/*  Title:      Pure/General/xml_data.scala
     1.5 -    Author:     Makarius
     1.6 -
     1.7 -XML as basic data representation language.
     1.8 -*/
     1.9 -
    1.10 -package isabelle
    1.11 -
    1.12 -
    1.13 -
    1.14 -object XML_Data
    1.15 -{
    1.16 -  /** encode **/
    1.17 -
    1.18 -  object Encode
    1.19 -  {
    1.20 -    type T[A] = A => XML.Body
    1.21 -
    1.22 -
    1.23 -    /* basic values */
    1.24 -
    1.25 -    private def long_atom(i: Long): String = i.toString
    1.26 -
    1.27 -    private def int_atom(i: Int): String = i.toString
    1.28 -
    1.29 -    private def bool_atom(b: Boolean): String = if (b) "1" else "0"
    1.30 -
    1.31 -    private def unit_atom(u: Unit) = ""
    1.32 -
    1.33 -
    1.34 -    /* structural nodes */
    1.35 -
    1.36 -    private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
    1.37 -
    1.38 -    private def tagged(tag: Int, ts: XML.Body): XML.Tree =
    1.39 -      XML.Elem(Markup(int_atom(tag), Nil), ts)
    1.40 -
    1.41 -
    1.42 -    /* representation of standard types */
    1.43 -
    1.44 -    val properties: T[List[(String, String)]] =
    1.45 -      (props => List(XML.Elem(Markup(":", props), Nil)))
    1.46 -
    1.47 -    val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
    1.48 -
    1.49 -    val long: T[Long] = (x => string(long_atom(x)))
    1.50 -
    1.51 -    val int: T[Int] = (x => string(int_atom(x)))
    1.52 -
    1.53 -    val bool: T[Boolean] = (x => string(bool_atom(x)))
    1.54 -
    1.55 -    val unit: T[Unit] = (x => string(unit_atom(x)))
    1.56 -
    1.57 -    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
    1.58 -      (x => List(node(f(x._1)), node(g(x._2))))
    1.59 -
    1.60 -    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
    1.61 -      (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3))))
    1.62 -
    1.63 -    def list[A](f: T[A]): T[List[A]] =
    1.64 -      (xs => xs.map((x: A) => node(f(x))))
    1.65 -
    1.66 -    def option[A](f: T[A]): T[Option[A]] =
    1.67 -    {
    1.68 -      case None => Nil
    1.69 -      case Some(x) => List(node(f(x)))
    1.70 -    }
    1.71 -
    1.72 -    def variant[A](fs: List[PartialFunction[A, XML.Body]]): T[A] =
    1.73 -    {
    1.74 -      case x =>
    1.75 -        val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
    1.76 -        List(tagged(tag, f(x)))
    1.77 -    }
    1.78 -  }
    1.79 -
    1.80 -
    1.81 -
    1.82 -  /** decode **/
    1.83 -
    1.84 -  class XML_Atom(s: String) extends Exception(s)
    1.85 -  class XML_Body(body: XML.Body) extends Exception
    1.86 -
    1.87 -  object Decode
    1.88 -  {
    1.89 -    type T[A] = XML.Body => A
    1.90 -
    1.91 -
    1.92 -     /* basic values */
    1.93 -
    1.94 -    private def long_atom(s: String): Long =
    1.95 -      try { java.lang.Long.parseLong(s) }
    1.96 -      catch { case e: NumberFormatException => throw new XML_Atom(s) }
    1.97 -
    1.98 -    private def int_atom(s: String): Int =
    1.99 -      try { Integer.parseInt(s) }
   1.100 -      catch { case e: NumberFormatException => throw new XML_Atom(s) }
   1.101 -
   1.102 -    private def bool_atom(s: String): Boolean =
   1.103 -      if (s == "1") true
   1.104 -      else if (s == "0") false
   1.105 -      else throw new XML_Atom(s)
   1.106 -
   1.107 -    private def unit_atom(s: String): Unit =
   1.108 -      if (s == "") () else throw new XML_Atom(s)
   1.109 -
   1.110 -
   1.111 -    /* structural nodes */
   1.112 -
   1.113 -    private def node(t: XML.Tree): XML.Body =
   1.114 -      t match {
   1.115 -        case XML.Elem(Markup(":", Nil), ts) => ts
   1.116 -        case _ => throw new XML_Body(List(t))
   1.117 -      }
   1.118 -
   1.119 -    private def tagged(t: XML.Tree): (Int, XML.Body) =
   1.120 -      t match {
   1.121 -        case XML.Elem(Markup(s, Nil), ts) => (int_atom(s), ts)
   1.122 -        case _ => throw new XML_Body(List(t))
   1.123 -      }
   1.124 -
   1.125 -
   1.126 -    /* representation of standard types */
   1.127 -
   1.128 -    val properties: T[List[(String, String)]] =
   1.129 -    {
   1.130 -      case List(XML.Elem(Markup(":", props), Nil)) => props
   1.131 -      case ts => throw new XML_Body(ts)
   1.132 -    }
   1.133 -
   1.134 -    val string: T[String] =
   1.135 -    {
   1.136 -      case Nil => ""
   1.137 -      case List(XML.Text(s)) => s
   1.138 -      case ts => throw new XML_Body(ts)
   1.139 -    }
   1.140 -
   1.141 -    val long: T[Long] = (x => long_atom(string(x)))
   1.142 -
   1.143 -    val int: T[Int] = (x => int_atom(string(x)))
   1.144 -
   1.145 -    val bool: T[Boolean] = (x => bool_atom(string(x)))
   1.146 -
   1.147 -    val unit: T[Unit] = (x => unit_atom(string(x)))
   1.148 -
   1.149 -    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
   1.150 -    {
   1.151 -      case List(t1, t2) => (f(node(t1)), g(node(t2)))
   1.152 -      case ts => throw new XML_Body(ts)
   1.153 -    }
   1.154 -
   1.155 -    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
   1.156 -    {
   1.157 -      case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
   1.158 -      case ts => throw new XML_Body(ts)
   1.159 -    }
   1.160 -
   1.161 -    def list[A](f: T[A]): T[List[A]] =
   1.162 -      (ts => ts.map(t => f(node(t))))
   1.163 -
   1.164 -    def option[A](f: T[A]): T[Option[A]] =
   1.165 -    {
   1.166 -      case Nil => None
   1.167 -      case List(t) => Some(f(node(t)))
   1.168 -      case ts => throw new XML_Body(ts)
   1.169 -    }
   1.170 -
   1.171 -    def variant[A](fs: List[T[A]]): T[A] =
   1.172 -    {
   1.173 -      case List(t) =>
   1.174 -        val (tag, ts) = tagged(t)
   1.175 -        fs(tag)(ts)
   1.176 -      case ts => throw new XML_Body(ts)
   1.177 -    }
   1.178 -  }
   1.179 -}