src/Pure/PIDE/xml.scala
author wenzelm
Sun May 13 16:37:36 2018 +0200 (13 months ago)
changeset 68169 395432e7516e
parent 67827 b027c97c77c9
child 68265 f0899dad4877
permissions -rw-r--r--
tuned signature;
wenzelm@44698
     1
/*  Title:      Pure/PIDE/xml.scala
wenzelm@27931
     2
    Author:     Makarius
wenzelm@27931
     3
wenzelm@44698
     4
Untyped XML trees and basic data representation.
wenzelm@27931
     5
*/
wenzelm@27931
     6
wenzelm@27931
     7
package isabelle
wenzelm@27931
     8
wenzelm@55618
     9
wenzelm@67109
    10
import java.util.{Collections, WeakHashMap}
wenzelm@34108
    11
import java.lang.ref.WeakReference
wenzelm@34108
    12
import javax.xml.parsers.DocumentBuilderFactory
wenzelm@34108
    13
wenzelm@27947
    14
wenzelm@29203
    15
object XML
wenzelm@29203
    16
{
wenzelm@43767
    17
  /** XML trees **/
wenzelm@43767
    18
wenzelm@27947
    19
  /* datatype representation */
wenzelm@27947
    20
wenzelm@65753
    21
  type Attribute = Properties.Entry
wenzelm@43780
    22
  type Attributes = Properties.T
wenzelm@27931
    23
wenzelm@57912
    24
  sealed abstract class Tree { override def toString: String = string_of_tree(this) }
wenzelm@64354
    25
  type Body = List[Tree]
wenzelm@64354
    26
  case class Elem(markup: Markup, body: Body) extends Tree
wenzelm@52890
    27
  {
wenzelm@52890
    28
    def name: String = markup.name
wenzelm@65753
    29
wenzelm@64358
    30
    def update_attributes(more_attributes: Attributes): Elem =
wenzelm@64358
    31
      if (more_attributes.isEmpty) this
wenzelm@64358
    32
      else Elem(markup.update_properties(more_attributes), body)
wenzelm@65753
    33
wenzelm@65772
    34
    def + (att: Attribute): Elem = Elem(markup + att, body)
wenzelm@52890
    35
  }
wenzelm@29204
    36
  case class Text(content: String) extends Tree
wenzelm@29203
    37
wenzelm@66196
    38
  def elem(markup: Markup): XML.Elem = XML.Elem(markup, Nil)
wenzelm@64354
    39
  def elem(name: String, body: Body): XML.Elem = XML.Elem(Markup(name, Nil), body)
wenzelm@64354
    40
  def elem(name: String): XML.Elem = XML.Elem(Markup(name, Nil), Nil)
wenzelm@38267
    41
wenzelm@29203
    42
wenzelm@49650
    43
  /* wrapped elements */
wenzelm@49650
    44
wenzelm@60215
    45
  val XML_ELEM = "xml_elem"
wenzelm@60215
    46
  val XML_NAME = "xml_name"
wenzelm@60215
    47
  val XML_BODY = "xml_body"
wenzelm@49650
    48
wenzelm@49650
    49
  object Wrapped_Elem
wenzelm@49650
    50
  {
wenzelm@49650
    51
    def apply(markup: Markup, body1: Body, body2: Body): XML.Elem =
wenzelm@61026
    52
      XML.Elem(Markup(XML_ELEM, (XML_NAME, markup.name) :: markup.properties),
wenzelm@61026
    53
        XML.Elem(Markup(XML_BODY, Nil), body1) :: body2)
wenzelm@49650
    54
wenzelm@49650
    55
    def unapply(tree: Tree): Option[(Markup, Body, Body)] =
wenzelm@49650
    56
      tree match {
wenzelm@49650
    57
        case
wenzelm@61026
    58
          XML.Elem(Markup(XML_ELEM, (XML_NAME, name) :: props),
wenzelm@61026
    59
            XML.Elem(Markup(XML_BODY, Nil), body1) :: body2) =>
wenzelm@49650
    60
          Some(Markup(name, props), body1, body2)
wenzelm@49650
    61
        case _ => None
wenzelm@49650
    62
      }
wenzelm@49650
    63
  }
wenzelm@49650
    64
wenzelm@67818
    65
  object Root_Elem
wenzelm@67818
    66
  {
wenzelm@67818
    67
    def apply(body: Body): XML.Elem = XML.Elem(Markup(XML_ELEM, Nil), body)
wenzelm@67818
    68
    def unapply(tree: Tree): Option[Body] =
wenzelm@67818
    69
      tree match {
wenzelm@67818
    70
        case XML.Elem(Markup(XML_ELEM, Nil), body) => Some(body)
wenzelm@67818
    71
        case _ => None
wenzelm@67818
    72
      }
wenzelm@67818
    73
  }
wenzelm@67818
    74
wenzelm@49650
    75
wenzelm@49650
    76
  /* traverse text */
wenzelm@49650
    77
wenzelm@49650
    78
  def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A =
wenzelm@49650
    79
  {
wenzelm@49650
    80
    def traverse(x: A, t: Tree): A =
wenzelm@49650
    81
      t match {
wenzelm@61026
    82
        case XML.Wrapped_Elem(_, _, ts) => (x /: ts)(traverse)
wenzelm@61026
    83
        case XML.Elem(_, ts) => (x /: ts)(traverse)
wenzelm@61026
    84
        case XML.Text(s) => op(x, s)
wenzelm@49650
    85
      }
wenzelm@49650
    86
    (a /: body)(traverse)
wenzelm@49650
    87
  }
wenzelm@49650
    88
wenzelm@49650
    89
  def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length }
wenzelm@49650
    90
wenzelm@49650
    91
wenzelm@49650
    92
  /* text content */
wenzelm@49650
    93
wenzelm@49650
    94
  def content(body: Body): String =
wenzelm@49650
    95
  {
wenzelm@49650
    96
    val text = new StringBuilder(text_length(body))
wenzelm@49650
    97
    traverse_text(body)(()) { case (_, s) => text.append(s) }
wenzelm@49650
    98
    text.toString
wenzelm@49650
    99
  }
wenzelm@49650
   100
wenzelm@49650
   101
  def content(tree: Tree): String = content(List(tree))
wenzelm@49650
   102
wenzelm@49650
   103
wenzelm@49650
   104
wenzelm@49650
   105
  /** string representation **/
wenzelm@29203
   106
wenzelm@65990
   107
  def output_char(c: Char, s: StringBuilder)
wenzelm@65990
   108
  {
wenzelm@65990
   109
    c match {
wenzelm@65990
   110
      case '<' => s ++= "&lt;"
wenzelm@65990
   111
      case '>' => s ++= "&gt;"
wenzelm@65990
   112
      case '&' => s ++= "&amp;"
wenzelm@65990
   113
      case '"' => s ++= "&quot;"
wenzelm@65990
   114
      case '\'' => s ++= "&apos;"
wenzelm@65990
   115
      case _ => s += c
wenzelm@65990
   116
    }
wenzelm@65990
   117
  }
wenzelm@65990
   118
wenzelm@65990
   119
  def output_string(str: String, s: StringBuilder)
wenzelm@65990
   120
  {
wenzelm@65990
   121
    if (str == null) s ++= str
wenzelm@65990
   122
    else str.iterator.foreach(c => output_char(c, s))
wenzelm@65990
   123
  }
wenzelm@65990
   124
wenzelm@38268
   125
  def string_of_body(body: Body): String =
wenzelm@38268
   126
  {
wenzelm@38268
   127
    val s = new StringBuilder
wenzelm@38268
   128
wenzelm@65990
   129
    def text(txt: String) { output_string(txt, s) }
wenzelm@65991
   130
    def elem(markup: Markup)
wenzelm@65991
   131
    {
wenzelm@65991
   132
      s ++= markup.name
wenzelm@65991
   133
      for ((a, b) <- markup.properties) {
wenzelm@65991
   134
        s += ' '; s ++= a; s += '='; s += '"'; text(b); s += '"'
wenzelm@65991
   135
      }
wenzelm@65991
   136
    }
wenzelm@38268
   137
    def tree(t: Tree): Unit =
wenzelm@38268
   138
      t match {
wenzelm@61026
   139
        case XML.Elem(markup, Nil) =>
wenzelm@65991
   140
          s += '<'; elem(markup); s ++= "/>"
wenzelm@61026
   141
        case XML.Elem(markup, ts) =>
wenzelm@65991
   142
          s += '<'; elem(markup); s += '>'
wenzelm@38268
   143
          ts.foreach(tree)
wenzelm@65991
   144
          s ++= "</"; s ++= markup.name; s += '>'
wenzelm@61026
   145
        case XML.Text(txt) => text(txt)
wenzelm@38268
   146
      }
wenzelm@38268
   147
    body.foreach(tree)
wenzelm@38268
   148
    s.toString
wenzelm@29203
   149
  }
wenzelm@29203
   150
wenzelm@38268
   151
  def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
wenzelm@27941
   152
wenzelm@27941
   153
wenzelm@44808
   154
wenzelm@44808
   155
  /** cache for partial sharing (weak table) **/
wenzelm@34108
   156
wenzelm@68169
   157
  def make_cache(initial_size: Int = 131071, max_string: Int = 100): Cache =
wenzelm@68169
   158
    new Cache(initial_size, max_string)
wenzelm@68169
   159
wenzelm@68169
   160
  class Cache private[XML](initial_size: Int, max_string: Int)
wenzelm@34108
   161
  {
wenzelm@67109
   162
    private val table =
wenzelm@67109
   163
      Collections.synchronizedMap(new WeakHashMap[Any, WeakReference[Any]](initial_size))
wenzelm@38446
   164
wenzelm@67113
   165
    def size: Int = table.size
wenzelm@67113
   166
wenzelm@44704
   167
    private def lookup[A](x: A): Option[A] =
wenzelm@44704
   168
    {
wenzelm@44704
   169
      val ref = table.get(x)
wenzelm@44704
   170
      if (ref == null) None
wenzelm@44704
   171
      else {
wenzelm@44704
   172
        val y = ref.asInstanceOf[WeakReference[A]].get
wenzelm@44704
   173
        if (y == null) None
wenzelm@44704
   174
        else Some(y)
wenzelm@38446
   175
      }
wenzelm@44704
   176
    }
wenzelm@44704
   177
    private def store[A](x: A): A =
wenzelm@44704
   178
    {
wenzelm@44704
   179
      table.put(x, new WeakReference[Any](x))
wenzelm@44704
   180
      x
wenzelm@44704
   181
    }
wenzelm@34108
   182
wenzelm@51663
   183
    private def cache_string(x: String): String =
wenzelm@67827
   184
      if (x == "") ""
wenzelm@67827
   185
      else if (x == "true") "true"
wenzelm@57909
   186
      else if (x == "false") "false"
wenzelm@57909
   187
      else if (x == "0.0") "0.0"
wenzelm@57909
   188
      else if (Library.is_small_int(x)) Library.signed_string_of_int(Integer.parseInt(x))
wenzelm@57909
   189
      else
wenzelm@57909
   190
        lookup(x) match {
wenzelm@57909
   191
          case Some(y) => y
wenzelm@57909
   192
          case None =>
wenzelm@65903
   193
            val z = Library.isolate_substring(x)
wenzelm@57909
   194
            if (z.length > max_string) z else store(z)
wenzelm@57909
   195
        }
wenzelm@51663
   196
    private def cache_props(x: Properties.T): Properties.T =
wenzelm@44704
   197
      if (x.isEmpty) x
wenzelm@44704
   198
      else
wenzelm@34133
   199
        lookup(x) match {
wenzelm@34133
   200
          case Some(y) => y
wenzelm@65903
   201
          case None => store(x.map(p => (Library.isolate_substring(p._1).intern, cache_string(p._2))))
wenzelm@34133
   202
        }
wenzelm@51663
   203
    private def cache_markup(x: Markup): Markup =
wenzelm@44704
   204
      lookup(x) match {
wenzelm@44704
   205
        case Some(y) => y
wenzelm@44704
   206
        case None =>
wenzelm@44704
   207
          x match {
wenzelm@44704
   208
            case Markup(name, props) =>
wenzelm@51663
   209
              store(Markup(cache_string(name), cache_props(props)))
wenzelm@44704
   210
          }
wenzelm@44704
   211
      }
wenzelm@51663
   212
    private def cache_tree(x: XML.Tree): XML.Tree =
wenzelm@44704
   213
      lookup(x) match {
wenzelm@44704
   214
        case Some(y) => y
wenzelm@44704
   215
        case None =>
wenzelm@44704
   216
          x match {
wenzelm@44704
   217
            case XML.Elem(markup, body) =>
wenzelm@51663
   218
              store(XML.Elem(cache_markup(markup), cache_body(body)))
wenzelm@51663
   219
            case XML.Text(text) => store(XML.Text(cache_string(text)))
wenzelm@44704
   220
          }
wenzelm@44704
   221
      }
wenzelm@51663
   222
    private def cache_body(x: XML.Body): XML.Body =
wenzelm@44704
   223
      if (x.isEmpty) x
wenzelm@44704
   224
      else
wenzelm@34133
   225
        lookup(x) match {
wenzelm@34133
   226
          case Some(y) => y
wenzelm@51663
   227
          case None => x.map(cache_tree(_))
wenzelm@34133
   228
        }
wenzelm@38446
   229
wenzelm@38446
   230
    // main methods
wenzelm@51663
   231
    def string(x: String): String = synchronized { cache_string(x) }
wenzelm@51663
   232
    def props(x: Properties.T): Properties.T = synchronized { cache_props(x) }
wenzelm@51663
   233
    def markup(x: Markup): Markup = synchronized { cache_markup(x) }
wenzelm@51663
   234
    def tree(x: XML.Tree): XML.Tree = synchronized { cache_tree(x) }
wenzelm@51663
   235
    def body(x: XML.Body): XML.Body = synchronized { cache_body(x) }
wenzelm@51663
   236
    def elem(x: XML.Elem): XML.Elem = synchronized { cache_tree(x).asInstanceOf[XML.Elem] }
wenzelm@34108
   237
  }
wenzelm@34108
   238
wenzelm@34108
   239
wenzelm@43767
   240
wenzelm@43767
   241
  /** XML as data representation language **/
wenzelm@43767
   242
wenzelm@51987
   243
  abstract class Error(s: String) extends Exception(s)
wenzelm@51987
   244
  class XML_Atom(s: String) extends Error(s)
wenzelm@51987
   245
  class XML_Body(body: XML.Body) extends Error("")
wenzelm@43767
   246
wenzelm@43767
   247
  object Encode
wenzelm@43767
   248
  {
wenzelm@43767
   249
    type T[A] = A => XML.Body
wenzelm@65334
   250
    type V[A] = PartialFunction[A, (List[String], XML.Body)]
wenzelm@43767
   251
wenzelm@43767
   252
wenzelm@43778
   253
    /* atomic values */
wenzelm@43767
   254
wenzelm@57909
   255
    def long_atom(i: Long): String = Library.signed_string_of_long(i)
wenzelm@43767
   256
wenzelm@57909
   257
    def int_atom(i: Int): String = Library.signed_string_of_int(i)
wenzelm@43767
   258
wenzelm@43778
   259
    def bool_atom(b: Boolean): String = if (b) "1" else "0"
wenzelm@43767
   260
wenzelm@43778
   261
    def unit_atom(u: Unit) = ""
wenzelm@43767
   262
wenzelm@43767
   263
wenzelm@43767
   264
    /* structural nodes */
wenzelm@43767
   265
wenzelm@43767
   266
    private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
wenzelm@43767
   267
wenzelm@43781
   268
    private def vector(xs: List[String]): XML.Attributes =
wenzelm@46839
   269
      xs.zipWithIndex.map({ case (x, i) => (int_atom(i), x) })
wenzelm@43778
   270
wenzelm@43778
   271
    private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree =
wenzelm@43778
   272
      XML.Elem(Markup(int_atom(tag), vector(data._1)), data._2)
wenzelm@43767
   273
wenzelm@43767
   274
wenzelm@43767
   275
    /* representation of standard types */
wenzelm@43767
   276
wenzelm@65333
   277
    val tree: T[XML.Tree] = (t => List(t))
wenzelm@65333
   278
wenzelm@43780
   279
    val properties: T[Properties.T] =
wenzelm@43767
   280
      (props => List(XML.Elem(Markup(":", props), Nil)))
wenzelm@43767
   281
wenzelm@43767
   282
    val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
wenzelm@43767
   283
wenzelm@43767
   284
    val long: T[Long] = (x => string(long_atom(x)))
wenzelm@43767
   285
wenzelm@43767
   286
    val int: T[Int] = (x => string(int_atom(x)))
wenzelm@43767
   287
wenzelm@43767
   288
    val bool: T[Boolean] = (x => string(bool_atom(x)))
wenzelm@43767
   289
wenzelm@43767
   290
    val unit: T[Unit] = (x => string(unit_atom(x)))
wenzelm@43767
   291
wenzelm@43767
   292
    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
wenzelm@43767
   293
      (x => List(node(f(x._1)), node(g(x._2))))
wenzelm@43767
   294
wenzelm@43767
   295
    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
wenzelm@43767
   296
      (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3))))
wenzelm@43767
   297
wenzelm@43767
   298
    def list[A](f: T[A]): T[List[A]] =
wenzelm@43767
   299
      (xs => xs.map((x: A) => node(f(x))))
wenzelm@43767
   300
wenzelm@43767
   301
    def option[A](f: T[A]): T[Option[A]] =
wenzelm@43767
   302
    {
wenzelm@43767
   303
      case None => Nil
wenzelm@43767
   304
      case Some(x) => List(node(f(x)))
wenzelm@43767
   305
    }
wenzelm@43767
   306
wenzelm@65334
   307
    def variant[A](fs: List[V[A]]): T[A] =
wenzelm@43767
   308
    {
wenzelm@43767
   309
      case x =>
wenzelm@43767
   310
        val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
wenzelm@43767
   311
        List(tagged(tag, f(x)))
wenzelm@43767
   312
    }
wenzelm@43767
   313
  }
wenzelm@43767
   314
wenzelm@43767
   315
  object Decode
wenzelm@43767
   316
  {
wenzelm@43767
   317
    type T[A] = XML.Body => A
wenzelm@43778
   318
    type V[A] = (List[String], XML.Body) => A
wenzelm@43767
   319
wenzelm@43767
   320
wenzelm@43778
   321
    /* atomic values */
wenzelm@43767
   322
wenzelm@43778
   323
    def long_atom(s: String): Long =
wenzelm@43767
   324
      try { java.lang.Long.parseLong(s) }
wenzelm@43767
   325
      catch { case e: NumberFormatException => throw new XML_Atom(s) }
wenzelm@43767
   326
wenzelm@43778
   327
    def int_atom(s: String): Int =
wenzelm@43767
   328
      try { Integer.parseInt(s) }
wenzelm@43767
   329
      catch { case e: NumberFormatException => throw new XML_Atom(s) }
wenzelm@43767
   330
wenzelm@43778
   331
    def bool_atom(s: String): Boolean =
wenzelm@43767
   332
      if (s == "1") true
wenzelm@43767
   333
      else if (s == "0") false
wenzelm@43767
   334
      else throw new XML_Atom(s)
wenzelm@43767
   335
wenzelm@43778
   336
    def unit_atom(s: String): Unit =
wenzelm@43767
   337
      if (s == "") () else throw new XML_Atom(s)
wenzelm@43767
   338
wenzelm@43767
   339
wenzelm@43767
   340
    /* structural nodes */
wenzelm@43767
   341
wenzelm@43767
   342
    private def node(t: XML.Tree): XML.Body =
wenzelm@43767
   343
      t match {
wenzelm@43767
   344
        case XML.Elem(Markup(":", Nil), ts) => ts
wenzelm@43767
   345
        case _ => throw new XML_Body(List(t))
wenzelm@43767
   346
      }
wenzelm@43767
   347
wenzelm@43781
   348
    private def vector(atts: XML.Attributes): List[String] =
wenzelm@46839
   349
      atts.iterator.zipWithIndex.map(
wenzelm@46839
   350
        { case ((a, x), i) => if (int_atom(a) == i) x else throw new XML_Atom(a) }).toList
wenzelm@43778
   351
wenzelm@43778
   352
    private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) =
wenzelm@43767
   353
      t match {
wenzelm@43781
   354
        case XML.Elem(Markup(name, atts), ts) => (int_atom(name), (vector(atts), ts))
wenzelm@43767
   355
        case _ => throw new XML_Body(List(t))
wenzelm@43767
   356
      }
wenzelm@43767
   357
wenzelm@43767
   358
wenzelm@43767
   359
    /* representation of standard types */
wenzelm@43767
   360
wenzelm@65333
   361
    val tree: T[XML.Tree] =
wenzelm@65333
   362
    {
wenzelm@65333
   363
      case List(t) => t
wenzelm@65333
   364
      case ts => throw new XML_Body(ts)
wenzelm@65333
   365
    }
wenzelm@65333
   366
wenzelm@43780
   367
    val properties: T[Properties.T] =
wenzelm@43767
   368
    {
wenzelm@43767
   369
      case List(XML.Elem(Markup(":", props), Nil)) => props
wenzelm@43767
   370
      case ts => throw new XML_Body(ts)
wenzelm@43767
   371
    }
wenzelm@43767
   372
wenzelm@43767
   373
    val string: T[String] =
wenzelm@43767
   374
    {
wenzelm@43767
   375
      case Nil => ""
wenzelm@43767
   376
      case List(XML.Text(s)) => s
wenzelm@43767
   377
      case ts => throw new XML_Body(ts)
wenzelm@43767
   378
    }
wenzelm@43767
   379
wenzelm@43767
   380
    val long: T[Long] = (x => long_atom(string(x)))
wenzelm@43767
   381
wenzelm@43767
   382
    val int: T[Int] = (x => int_atom(string(x)))
wenzelm@43767
   383
wenzelm@43767
   384
    val bool: T[Boolean] = (x => bool_atom(string(x)))
wenzelm@43767
   385
wenzelm@43767
   386
    val unit: T[Unit] = (x => unit_atom(string(x)))
wenzelm@43767
   387
wenzelm@43767
   388
    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
wenzelm@43767
   389
    {
wenzelm@43767
   390
      case List(t1, t2) => (f(node(t1)), g(node(t2)))
wenzelm@43767
   391
      case ts => throw new XML_Body(ts)
wenzelm@43767
   392
    }
wenzelm@43767
   393
wenzelm@43767
   394
    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
wenzelm@43767
   395
    {
wenzelm@43767
   396
      case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
wenzelm@43767
   397
      case ts => throw new XML_Body(ts)
wenzelm@43767
   398
    }
wenzelm@43767
   399
wenzelm@43767
   400
    def list[A](f: T[A]): T[List[A]] =
wenzelm@43767
   401
      (ts => ts.map(t => f(node(t))))
wenzelm@43767
   402
wenzelm@43767
   403
    def option[A](f: T[A]): T[Option[A]] =
wenzelm@43767
   404
    {
wenzelm@43767
   405
      case Nil => None
wenzelm@43767
   406
      case List(t) => Some(f(node(t)))
wenzelm@43767
   407
      case ts => throw new XML_Body(ts)
wenzelm@43767
   408
    }
wenzelm@43767
   409
wenzelm@43778
   410
    def variant[A](fs: List[V[A]]): T[A] =
wenzelm@43767
   411
    {
wenzelm@43767
   412
      case List(t) =>
wenzelm@43778
   413
        val (tag, (xs, ts)) = tagged(t)
wenzelm@43768
   414
        val f =
wenzelm@43768
   415
          try { fs(tag) }
wenzelm@43768
   416
          catch { case _: IndexOutOfBoundsException => throw new XML_Body(List(t)) }
wenzelm@43778
   417
        f(xs, ts)
wenzelm@43767
   418
      case ts => throw new XML_Body(ts)
wenzelm@43767
   419
    }
wenzelm@43767
   420
  }
wenzelm@27931
   421
}