type XML.Body as basic data representation language (Scala version);
authorwenzelm
Tue Aug 10 23:03:48 2010 +0200 (2010-08-10)
changeset 38267e50c283dd125
parent 38266 492d377ecfe2
child 38268 beb86b805590
type XML.Body as basic data representation language (Scala version);
tuned;
src/Pure/General/xml.scala
src/Pure/General/xml_data.ML
src/Pure/General/xml_data.scala
src/Pure/General/yxml.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/General/xml.scala	Tue Aug 10 22:26:23 2010 +0200
     1.2 +++ b/src/Pure/General/xml.scala	Tue Aug 10 23:03:48 2010 +0200
     1.3 @@ -30,6 +30,8 @@
     1.4    def elem(name: String, body: List[Tree]) = Elem(Markup(name, Nil), body)
     1.5    def elem(name: String) = Elem(Markup(name, Nil), Nil)
     1.6  
     1.7 +  type Body = List[Tree]
     1.8 +
     1.9  
    1.10    /* string representation */
    1.11  
     2.1 --- a/src/Pure/General/xml_data.ML	Tue Aug 10 22:26:23 2010 +0200
     2.2 +++ b/src/Pure/General/xml_data.ML	Tue Aug 10 23:03:48 2010 +0200
     2.3 @@ -53,6 +53,7 @@
     2.4    | dest_bool_atom "1" = true
     2.5    | dest_bool_atom s = raise XML_ATOM s;
     2.6  
     2.7 +
     2.8  fun make_unit_atom () = "";
     2.9  
    2.10  fun dest_unit_atom "" = ()
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/General/xml_data.scala	Tue Aug 10 23:03:48 2010 +0200
     3.3 @@ -0,0 +1,124 @@
     3.4 +/*  Title:      Pure/General/xml_data.scala
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +XML as basic data representation language.
     3.8 +*/
     3.9 +
    3.10 +package isabelle
    3.11 +
    3.12 +
    3.13 +
    3.14 +object XML_Data
    3.15 +{
    3.16 +  /* basic values */
    3.17 +
    3.18 +  class XML_Atom(s: String) extends Exception(s)
    3.19 +
    3.20 +
    3.21 +  private def make_int_atom(i: Int): String = i.toString
    3.22 +
    3.23 +  private def dest_int_atom(s: String): Int =
    3.24 +    try { Integer.parseInt(s) }
    3.25 +    catch { case e: NumberFormatException => throw new XML_Atom(s) }
    3.26 +
    3.27 +
    3.28 +  private def make_bool_atom(b: Boolean): String = if (b) "1" else "0"
    3.29 +
    3.30 +  private def dest_bool_atom(s: String): Boolean =
    3.31 +    if (s == "1") true
    3.32 +    else if (s == "0") false
    3.33 +    else throw new XML_Atom(s)
    3.34 +
    3.35 +
    3.36 +  private def make_unit_atom(u: Unit) = ""
    3.37 +
    3.38 +  private def dest_unit_atom(s: String): Unit =
    3.39 +    if (s == "") () else throw new XML_Atom(s)
    3.40 +
    3.41 +
    3.42 +  /* structural nodes */
    3.43 +
    3.44 +  class XML_Body extends Exception  // FIXME exception argument!?
    3.45 +
    3.46 +  private def make_node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
    3.47 +
    3.48 +  private def dest_node(t: XML.Tree): XML.Body =
    3.49 +    t match {
    3.50 +      case XML.Elem(Markup(":", Nil), ts) => ts
    3.51 +      case _ => throw new XML_Body
    3.52 +    }
    3.53 +
    3.54 +
    3.55 +  /* representation of standard types */
    3.56 +
    3.57 +  def make_properties(props: List[(String, String)]): XML.Body =
    3.58 +    List(XML.Elem(Markup(":", props), Nil))
    3.59 +
    3.60 +  def dest_properties(ts: XML.Body): List[(String, String)] =
    3.61 +    ts match {
    3.62 +      case List(XML.Elem(Markup(":", props), Nil)) => props
    3.63 +      case _ => throw new XML_Body
    3.64 +    }
    3.65 +
    3.66 +
    3.67 +  def make_string(s: String): XML.Body = List(XML.Text(s))
    3.68 +
    3.69 +  def dest_string(ts: XML.Body): String =
    3.70 +    ts match {
    3.71 +      case List(XML.Text(s)) => s
    3.72 +      case _ => throw new XML_Body
    3.73 +    }
    3.74 +
    3.75 +
    3.76 +  def make_int(i: Int): XML.Body = make_string(make_int_atom(i))
    3.77 +  def dest_int(ts: XML.Body): Int = dest_int_atom(dest_string(ts))
    3.78 +
    3.79 +  def make_bool(b: Boolean): XML.Body = make_string(make_bool_atom(b))
    3.80 +  def dest_bool(ts: XML.Body) = dest_bool_atom(dest_string(ts))
    3.81 +
    3.82 +  def make_unit(u: Unit): XML.Body = make_string(make_unit_atom(u))
    3.83 +  def dest_unit(ts: XML.Body): Unit = dest_unit_atom(dest_string(ts))
    3.84 +
    3.85 +
    3.86 +  def make_pair[A, B](make1: A => XML.Body)(make2: B => XML.Body)(p: (A, B)): XML.Body =
    3.87 +    List(make_node(make1(p._1)), make_node(make2(p._2)))
    3.88 +
    3.89 +  def dest_pair[A, B](dest1: XML.Body => A)(dest2: XML.Body => B)(ts: XML.Body): (A, B) =
    3.90 +    ts match {
    3.91 +      case List(t1, t2) => (dest1(dest_node(t1)), dest2(dest_node(t2)))
    3.92 +      case _ => throw new XML_Body
    3.93 +    }
    3.94 +
    3.95 +
    3.96 +  def make_triple[A, B, C](make1: A => XML.Body)(make2: B => XML.Body)(make3: C => XML.Body)
    3.97 +      (p: (A, B, C)): XML.Body =
    3.98 +    List(make_node(make1(p._1)), make_node(make2(p._2)), make_node(make3(p._3)))
    3.99 +
   3.100 +  def dest_triple[A, B, C](dest1: XML.Body => A)(dest2: XML.Body => B)(dest3: XML.Body => C)
   3.101 +      (ts: XML.Body): (A, B, C) =
   3.102 +    ts match {
   3.103 +      case List(t1, t2, t3) => (dest1(dest_node(t1)), dest2(dest_node(t2)), dest3(dest_node(t3)))
   3.104 +      case _ => throw new XML_Body
   3.105 +    }
   3.106 +
   3.107 +
   3.108 +  def make_list[A](make: A => XML.Body)(xs: List[A]): XML.Body =
   3.109 +    xs.map((x: A) => make_node(make(x)))
   3.110 +
   3.111 +  def dest_list[A](dest: XML.Body => A)(ts: XML.Body): List[A] =
   3.112 +    ts.map((t: XML.Tree) => dest(dest_node(t)))
   3.113 +
   3.114 +
   3.115 +  def make_option[A](make: A => XML.Body)(opt: Option[A]): XML.Body =
   3.116 +    opt match {
   3.117 +      case None => make_list(make)(Nil)
   3.118 +      case Some(x) => make_list(make)(List(x))
   3.119 +    }
   3.120 +
   3.121 +  def dest_option[A](dest: XML.Body => A)(ts: XML.Body): Option[A] =
   3.122 +    dest_list(dest)(ts) match {
   3.123 +      case Nil => None
   3.124 +      case List(x) => Some(x)
   3.125 +      case _ => throw new XML_Body
   3.126 +    }
   3.127 +}
     4.1 --- a/src/Pure/General/yxml.scala	Tue Aug 10 22:26:23 2010 +0200
     4.2 +++ b/src/Pure/General/yxml.scala	Tue Aug 10 23:03:48 2010 +0200
     4.3 @@ -59,7 +59,7 @@
     4.4    }
     4.5  
     4.6  
     4.7 -  def parse_body(source: CharSequence): List[XML.Tree] =
     4.8 +  def parse_body(source: CharSequence): XML.Body =
     4.9    {
    4.10      /* stack operations */
    4.11  
    4.12 @@ -120,7 +120,7 @@
    4.13      XML.elem (Markup.MALFORMED,
    4.14        List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
    4.15  
    4.16 -  def parse_body_failsafe(source: CharSequence): List[XML.Tree] =
    4.17 +  def parse_body_failsafe(source: CharSequence): XML.Body =
    4.18    {
    4.19      try { parse_body(source) }
    4.20      catch { case _: RuntimeException => List(markup_failsafe(source)) }
     5.1 --- a/src/Pure/build-jars	Tue Aug 10 22:26:23 2010 +0200
     5.2 +++ b/src/Pure/build-jars	Tue Aug 10 23:03:48 2010 +0200
     5.3 @@ -31,6 +31,7 @@
     5.4    General/scan.scala
     5.5    General/symbol.scala
     5.6    General/xml.scala
     5.7 +  General/xml_data.scala
     5.8    General/yxml.scala
     5.9    Isar/isar_document.scala
    5.10    Isar/keyword.scala