--- a/src/Pure/General/xml_data.scala Sun Jul 10 13:00:22 2011 +0200
+++ b/src/Pure/General/xml_data.scala Sun Jul 10 13:51:21 2011 +0200
@@ -10,150 +10,162 @@
object XML_Data
{
- /* basic values */
+ /** make **/
- class XML_Atom(s: String) extends Exception(s)
-
+ object Make
+ {
+ /* basic values */
- private def make_long_atom(i: Long): String = i.toString
+ private def long_atom(i: Long): String = i.toString
+
+ private def int_atom(i: Int): String = i.toString
- private def dest_long_atom(s: String): Long =
- try { java.lang.Long.parseLong(s) }
- catch { case e: NumberFormatException => throw new XML_Atom(s) }
+ private def bool_atom(b: Boolean): String = if (b) "1" else "0"
+
+ private def unit_atom(u: Unit) = ""
- private def make_int_atom(i: Int): String = i.toString
-
- private def dest_int_atom(s: String): Int =
- try { Integer.parseInt(s) }
- catch { case e: NumberFormatException => throw new XML_Atom(s) }
-
-
- private def make_bool_atom(b: Boolean): String = if (b) "1" else "0"
+ /* structural nodes */
- private def dest_bool_atom(s: String): Boolean =
- if (s == "1") true
- else if (s == "0") false
- else throw new XML_Atom(s)
+ private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
-
- private def make_unit_atom(u: Unit) = ""
-
- private def dest_unit_atom(s: String): Unit =
- if (s == "") () else throw new XML_Atom(s)
+ private def tagged(tag: Int, ts: XML.Body): XML.Tree =
+ XML.Elem(Markup(int_atom(tag), Nil), ts)
- /* structural nodes */
+ /* representation of standard types */
- class XML_Body(body: XML.Body) extends Exception
+ def properties(props: List[(String, String)]): XML.Body =
+ List(XML.Elem(Markup(":", props), Nil))
- private def make_node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
+ 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))
- private def dest_node(t: XML.Tree): XML.Body =
- t match {
- case XML.Elem(Markup(":", Nil), ts) => ts
- case _ => throw new XML_Body(List(t))
- }
+ def int(i: Int): XML.Body = string(int_atom(i))
+
+ def bool(b: Boolean): XML.Body = string(bool_atom(b))
- private def make_tagged(tag: Int, ts: XML.Body): XML.Tree =
- XML.Elem(Markup(make_int_atom(tag), Nil), ts)
+ 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)))
- private def dest_tagged(t: XML.Tree): (Int, XML.Body) =
- t match {
- case XML.Elem(Markup(s, Nil), ts) => (dest_int_atom(s), ts)
- case _ => throw new XML_Body(List(t))
- }
+ 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)))
-
- /* representation of standard types */
+ def list[A](f: A => XML.Body)(xs: List[A]): XML.Body =
+ xs.map((x: A) => node(f(x)))
- def make_properties(props: List[(String, String)]): XML.Body =
- List(XML.Elem(Markup(":", props), Nil))
+ 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 dest_properties(ts: XML.Body): List[(String, String)] =
- ts match {
- case List(XML.Elem(Markup(":", props), Nil)) => props
- case _ => throw new XML_Body(ts)
+ 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)))
}
+ }
+
- def make_string(s: String): XML.Body = if (s.isEmpty) Nil else List(XML.Text(s))
+ /** dest **/
+
+ class XML_Atom(s: String) extends Exception(s)
+ class XML_Body(body: XML.Body) extends Exception
+
+ object Dest
+ {
+ /* basic values */
- def dest_string(ts: XML.Body): String =
- ts match {
- case Nil => ""
- case List(XML.Text(s)) => s
- case _ => throw new XML_Body(ts)
- }
+ 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)
- def make_long(i: Long): XML.Body = make_string(make_long_atom(i))
- def dest_long(ts: XML.Body): Long = dest_long_atom(dest_string(ts))
-
- def make_int(i: Int): XML.Body = make_string(make_int_atom(i))
- def dest_int(ts: XML.Body): Int = dest_int_atom(dest_string(ts))
-
- def make_bool(b: Boolean): XML.Body = make_string(make_bool_atom(b))
- def dest_bool(ts: XML.Body) = dest_bool_atom(dest_string(ts))
+ /* structural nodes */
- def make_unit(u: Unit): XML.Body = make_string(make_unit_atom(u))
- def dest_unit(ts: XML.Body): Unit = dest_unit_atom(dest_string(ts))
-
+ private def node(t: XML.Tree): XML.Body =
+ t match {
+ case XML.Elem(Markup(":", Nil), ts) => ts
+ case _ => throw new XML_Body(List(t))
+ }
- def make_pair[A, B](make1: A => XML.Body, make2: B => XML.Body)(p: (A, B)): XML.Body =
- List(make_node(make1(p._1)), make_node(make2(p._2)))
-
- def dest_pair[A, B](dest1: XML.Body => A, dest2: XML.Body => B)(ts: XML.Body): (A, B) =
- ts match {
- case List(t1, t2) => (dest1(dest_node(t1)), dest2(dest_node(t2)))
- case _ => throw new XML_Body(ts)
- }
+ 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))
+ }
- def make_triple[A, B, C](make1: A => XML.Body, make2: B => XML.Body, make3: C => XML.Body)
- (p: (A, B, C)): XML.Body =
- List(make_node(make1(p._1)), make_node(make2(p._2)), make_node(make3(p._3)))
+ /* 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 dest_triple[A, B, C](dest1: XML.Body => A, dest2: XML.Body => B, dest3: XML.Body => C)
- (ts: XML.Body): (A, B, C) =
- ts match {
- case List(t1, t2, t3) => (dest1(dest_node(t1)), dest2(dest_node(t2)), dest3(dest_node(t3)))
- 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 make_list[A](make: A => XML.Body)(xs: List[A]): XML.Body =
- xs.map((x: A) => make_node(make(x)))
+ def int(ts: XML.Body): Int = int_atom(string(ts))
- def dest_list[A](dest: XML.Body => A)(ts: XML.Body): List[A] =
- ts.map((t: XML.Tree) => dest(dest_node(t)))
+ def bool(ts: XML.Body) = bool_atom(string(ts))
+ def unit(ts: XML.Body): Unit = unit_atom(string(ts))
- def make_option[A](make: A => XML.Body)(opt: Option[A]): XML.Body =
- opt match {
- case None => Nil
- case Some(x) => List(make_node(make(x)))
- }
+ 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 dest_option[A](dest: XML.Body => A)(ts: XML.Body): Option[A] =
- ts match {
- case Nil => None
- case List(t) => Some(dest(dest_node(t)))
- 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 make_variant[A](makes: List[PartialFunction[A, XML.Body]])(x: A): XML.Body =
- {
- val (make, tag) = makes.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
- List(make_tagged(tag, make(x)))
- }
+ 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 dest_variant[A](dests: List[XML.Body => A])(ts: XML.Body): A =
- ts match {
- case List(t) =>
- val (tag, ts) = dest_tagged(t)
- dests(tag)(ts)
- 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)
+ }
+ }
}