src/Pure/General/xml_data.scala
author wenzelm
Wed Aug 11 22:41:26 2010 +0200 (2010-08-11)
changeset 38355 8cb265fb12fe
parent 38269 cd6906d9199f
child 43698 91c4d7397f0e
permissions -rw-r--r--
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm@38267
     1
/*  Title:      Pure/General/xml_data.scala
wenzelm@38267
     2
    Author:     Makarius
wenzelm@38267
     3
wenzelm@38267
     4
XML as basic data representation language.
wenzelm@38267
     5
*/
wenzelm@38267
     6
wenzelm@38267
     7
package isabelle
wenzelm@38267
     8
wenzelm@38267
     9
wenzelm@38267
    10
wenzelm@38267
    11
object XML_Data
wenzelm@38267
    12
{
wenzelm@38267
    13
  /* basic values */
wenzelm@38267
    14
wenzelm@38267
    15
  class XML_Atom(s: String) extends Exception(s)
wenzelm@38267
    16
wenzelm@38267
    17
wenzelm@38355
    18
  private def make_long_atom(i: Long): String = i.toString
wenzelm@38355
    19
wenzelm@38355
    20
  private def dest_long_atom(s: String): Long =
wenzelm@38355
    21
    try { java.lang.Long.parseLong(s) }
wenzelm@38355
    22
    catch { case e: NumberFormatException => throw new XML_Atom(s) }
wenzelm@38355
    23
wenzelm@38355
    24
wenzelm@38267
    25
  private def make_int_atom(i: Int): String = i.toString
wenzelm@38267
    26
wenzelm@38267
    27
  private def dest_int_atom(s: String): Int =
wenzelm@38267
    28
    try { Integer.parseInt(s) }
wenzelm@38267
    29
    catch { case e: NumberFormatException => throw new XML_Atom(s) }
wenzelm@38267
    30
wenzelm@38267
    31
wenzelm@38267
    32
  private def make_bool_atom(b: Boolean): String = if (b) "1" else "0"
wenzelm@38267
    33
wenzelm@38267
    34
  private def dest_bool_atom(s: String): Boolean =
wenzelm@38267
    35
    if (s == "1") true
wenzelm@38267
    36
    else if (s == "0") false
wenzelm@38267
    37
    else throw new XML_Atom(s)
wenzelm@38267
    38
wenzelm@38267
    39
wenzelm@38267
    40
  private def make_unit_atom(u: Unit) = ""
wenzelm@38267
    41
wenzelm@38267
    42
  private def dest_unit_atom(s: String): Unit =
wenzelm@38267
    43
    if (s == "") () else throw new XML_Atom(s)
wenzelm@38267
    44
wenzelm@38267
    45
wenzelm@38267
    46
  /* structural nodes */
wenzelm@38267
    47
wenzelm@38269
    48
  class XML_Body(body: XML.Body) extends Exception
wenzelm@38267
    49
wenzelm@38267
    50
  private def make_node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
wenzelm@38267
    51
wenzelm@38267
    52
  private def dest_node(t: XML.Tree): XML.Body =
wenzelm@38267
    53
    t match {
wenzelm@38267
    54
      case XML.Elem(Markup(":", Nil), ts) => ts
wenzelm@38269
    55
      case _ => throw new XML_Body(List(t))
wenzelm@38267
    56
    }
wenzelm@38267
    57
wenzelm@38267
    58
wenzelm@38267
    59
  /* representation of standard types */
wenzelm@38267
    60
wenzelm@38267
    61
  def make_properties(props: List[(String, String)]): XML.Body =
wenzelm@38267
    62
    List(XML.Elem(Markup(":", props), Nil))
wenzelm@38267
    63
wenzelm@38267
    64
  def dest_properties(ts: XML.Body): List[(String, String)] =
wenzelm@38267
    65
    ts match {
wenzelm@38267
    66
      case List(XML.Elem(Markup(":", props), Nil)) => props
wenzelm@38269
    67
      case _ => throw new XML_Body(ts)
wenzelm@38267
    68
    }
wenzelm@38267
    69
wenzelm@38267
    70
wenzelm@38269
    71
  def make_string(s: String): XML.Body = if (s.isEmpty) Nil else List(XML.Text(s))
wenzelm@38267
    72
wenzelm@38267
    73
  def dest_string(ts: XML.Body): String =
wenzelm@38267
    74
    ts match {
wenzelm@38269
    75
      case Nil => ""
wenzelm@38267
    76
      case List(XML.Text(s)) => s
wenzelm@38269
    77
      case _ => throw new XML_Body(ts)
wenzelm@38267
    78
    }
wenzelm@38267
    79
wenzelm@38267
    80
wenzelm@38355
    81
  def make_long(i: Long): XML.Body = make_string(make_long_atom(i))
wenzelm@38355
    82
  def dest_long(ts: XML.Body): Long = dest_long_atom(dest_string(ts))
wenzelm@38355
    83
wenzelm@38267
    84
  def make_int(i: Int): XML.Body = make_string(make_int_atom(i))
wenzelm@38267
    85
  def dest_int(ts: XML.Body): Int = dest_int_atom(dest_string(ts))
wenzelm@38267
    86
wenzelm@38267
    87
  def make_bool(b: Boolean): XML.Body = make_string(make_bool_atom(b))
wenzelm@38267
    88
  def dest_bool(ts: XML.Body) = dest_bool_atom(dest_string(ts))
wenzelm@38267
    89
wenzelm@38267
    90
  def make_unit(u: Unit): XML.Body = make_string(make_unit_atom(u))
wenzelm@38267
    91
  def dest_unit(ts: XML.Body): Unit = dest_unit_atom(dest_string(ts))
wenzelm@38267
    92
wenzelm@38267
    93
wenzelm@38267
    94
  def make_pair[A, B](make1: A => XML.Body)(make2: B => XML.Body)(p: (A, B)): XML.Body =
wenzelm@38267
    95
    List(make_node(make1(p._1)), make_node(make2(p._2)))
wenzelm@38267
    96
wenzelm@38267
    97
  def dest_pair[A, B](dest1: XML.Body => A)(dest2: XML.Body => B)(ts: XML.Body): (A, B) =
wenzelm@38267
    98
    ts match {
wenzelm@38267
    99
      case List(t1, t2) => (dest1(dest_node(t1)), dest2(dest_node(t2)))
wenzelm@38269
   100
      case _ => throw new XML_Body(ts)
wenzelm@38267
   101
    }
wenzelm@38267
   102
wenzelm@38267
   103
wenzelm@38267
   104
  def make_triple[A, B, C](make1: A => XML.Body)(make2: B => XML.Body)(make3: C => XML.Body)
wenzelm@38267
   105
      (p: (A, B, C)): XML.Body =
wenzelm@38267
   106
    List(make_node(make1(p._1)), make_node(make2(p._2)), make_node(make3(p._3)))
wenzelm@38267
   107
wenzelm@38267
   108
  def dest_triple[A, B, C](dest1: XML.Body => A)(dest2: XML.Body => B)(dest3: XML.Body => C)
wenzelm@38267
   109
      (ts: XML.Body): (A, B, C) =
wenzelm@38267
   110
    ts match {
wenzelm@38267
   111
      case List(t1, t2, t3) => (dest1(dest_node(t1)), dest2(dest_node(t2)), dest3(dest_node(t3)))
wenzelm@38269
   112
      case _ => throw new XML_Body(ts)
wenzelm@38267
   113
    }
wenzelm@38267
   114
wenzelm@38267
   115
wenzelm@38267
   116
  def make_list[A](make: A => XML.Body)(xs: List[A]): XML.Body =
wenzelm@38267
   117
    xs.map((x: A) => make_node(make(x)))
wenzelm@38267
   118
wenzelm@38267
   119
  def dest_list[A](dest: XML.Body => A)(ts: XML.Body): List[A] =
wenzelm@38267
   120
    ts.map((t: XML.Tree) => dest(dest_node(t)))
wenzelm@38267
   121
wenzelm@38267
   122
wenzelm@38267
   123
  def make_option[A](make: A => XML.Body)(opt: Option[A]): XML.Body =
wenzelm@38267
   124
    opt match {
wenzelm@38267
   125
      case None => make_list(make)(Nil)
wenzelm@38267
   126
      case Some(x) => make_list(make)(List(x))
wenzelm@38267
   127
    }
wenzelm@38267
   128
wenzelm@38267
   129
  def dest_option[A](dest: XML.Body => A)(ts: XML.Body): Option[A] =
wenzelm@38267
   130
    dest_list(dest)(ts) match {
wenzelm@38267
   131
      case Nil => None
wenzelm@38267
   132
      case List(x) => Some(x)
wenzelm@38269
   133
      case _ => throw new XML_Body(ts)
wenzelm@38267
   134
    }
wenzelm@38267
   135
}