src/Pure/PIDE/xml.scala
author nipkow
Fri, 21 Jun 2013 09:00:26 +0200
changeset 52402 c2f30ba4bb98
parent 51987 7d8e0e3c553b
child 52890 36e2c0c308eb
permissions -rw-r--r--
tuned
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
44698
0385292321a0 moved XML/YXML to src/Pure/PIDE;
wenzelm
parents: 44697
diff changeset
     1
/*  Title:      Pure/PIDE/xml.scala
45673
cd41e3903fbf separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
wenzelm
parents: 45667
diff changeset
     2
    Module:     PIDE
27931
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
     4
44698
0385292321a0 moved XML/YXML to src/Pure/PIDE;
wenzelm
parents: 44697
diff changeset
     5
Untyped XML trees and basic data representation.
27931
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
     6
*/
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
     7
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
     8
package isabelle
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
     9
34108
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
    10
import java.util.WeakHashMap
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
    11
import java.lang.ref.WeakReference
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
    12
import javax.xml.parsers.DocumentBuilderFactory
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
    13
27947
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
    14
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    15
object XML
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    16
{
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
    17
  /** XML trees **/
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
    18
27947
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
    19
  /* datatype representation */
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
    20
43780
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43778
diff changeset
    21
  type Attributes = Properties.T
27931
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
    22
38268
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    23
  sealed abstract class Tree { override def toString = string_of_tree(this) }
38230
ed147003de4b simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents: 36817
diff changeset
    24
  case class Elem(markup: Markup, body: List[Tree]) extends Tree
29204
wenzelm
parents: 29203
diff changeset
    25
  case class Text(content: String) extends Tree
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    26
38230
ed147003de4b simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents: 36817
diff changeset
    27
  def elem(name: String, body: List[Tree]) = Elem(Markup(name, Nil), body)
ed147003de4b simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents: 36817
diff changeset
    28
  def elem(name: String) = Elem(Markup(name, Nil), Nil)
33999
d3b200894e21 added auxiliary constructors;
wenzelm
parents: 33953
diff changeset
    29
38267
e50c283dd125 type XML.Body as basic data representation language (Scala version);
wenzelm
parents: 38263
diff changeset
    30
  type Body = List[Tree]
e50c283dd125 type XML.Body as basic data representation language (Scala version);
wenzelm
parents: 38263
diff changeset
    31
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    32
49650
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    33
  /* wrapped elements */
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    34
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    35
  val XML_ELEM = "xml_elem";
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    36
  val XML_NAME = "xml_name";
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    37
  val XML_BODY = "xml_body";
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    38
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    39
  object Wrapped_Elem
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    40
  {
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    41
    def apply(markup: Markup, body1: Body, body2: Body): XML.Elem =
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    42
      Elem(Markup(XML_ELEM, (XML_NAME, markup.name) :: markup.properties),
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    43
        Elem(Markup(XML_BODY, Nil), body1) :: body2)
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    44
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    45
    def unapply(tree: Tree): Option[(Markup, Body, Body)] =
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    46
      tree match {
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    47
        case
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    48
          Elem(Markup(XML_ELEM, (XML_NAME, name) :: props),
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    49
            Elem(Markup(XML_BODY, Nil), body1) :: body2) =>
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    50
          Some(Markup(name, props), body1, body2)
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    51
        case _ => None
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    52
      }
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    53
  }
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    54
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    55
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    56
  /* traverse text */
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    57
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    58
  def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A =
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    59
  {
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    60
    def traverse(x: A, t: Tree): A =
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    61
      t match {
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    62
        case Wrapped_Elem(_, _, ts) => (x /: ts)(traverse)
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    63
        case Elem(_, ts) => (x /: ts)(traverse)
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    64
        case Text(s) => op(x, s)
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    65
      }
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    66
    (a /: body)(traverse)
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    67
  }
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    68
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    69
  def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length }
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    70
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    71
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    72
  /* text content */
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    73
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    74
  def content(body: Body): String =
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    75
  {
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    76
    val text = new StringBuilder(text_length(body))
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    77
    traverse_text(body)(()) { case (_, s) => text.append(s) }
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    78
    text.toString
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    79
  }
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    80
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    81
  def content(tree: Tree): String = content(List(tree))
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    82
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    83
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    84
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49613
diff changeset
    85
  /** string representation **/
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    86
38268
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    87
  def string_of_body(body: Body): String =
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    88
  {
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    89
    val s = new StringBuilder
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    90
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    91
    def text(txt: String) {
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    92
      if (txt == null) s ++= txt
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    93
      else {
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    94
        for (c <- txt.iterator) c match {
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    95
          case '<' => s ++= "&lt;"
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    96
          case '>' => s ++= "&gt;"
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    97
          case '&' => s ++= "&amp;"
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    98
          case '"' => s ++= "&quot;"
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    99
          case '\'' => s ++= "&apos;"
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
   100
          case _ => s += c
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
   101
        }
34005
ada5098506af toString: more robust handling of null;
wenzelm
parents: 33999
diff changeset
   102
      }
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
   103
    }
38268
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
   104
    def attrib(p: (String, String)) { s ++= " "; s ++= p._1; s ++= "=\""; text(p._2); s ++= "\"" }
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
   105
    def elem(markup: Markup) { s ++= markup.name; markup.properties.foreach(attrib) }
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
   106
    def tree(t: Tree): Unit =
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
   107
      t match {
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
   108
        case Elem(markup, Nil) =>
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
   109
          s ++= "<"; elem(markup); s ++= "/>"
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
   110
        case Elem(markup, ts) =>
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
   111
          s ++= "<"; elem(markup); s ++= ">"
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
   112
          ts.foreach(tree)
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
   113
          s ++= "</"; s ++= markup.name; s ++= ">"
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
   114
        case Text(txt) => text(txt)
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
   115
      }
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
   116
    body.foreach(tree)
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
   117
    s.toString
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
   118
  }
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
   119
38268
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
   120
  def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
27941
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
   121
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
   122
44808
05b8997899a2 XML.cache for partial sharing (strings only);
wenzelm
parents: 44721
diff changeset
   123
05b8997899a2 XML.cache for partial sharing (strings only);
wenzelm
parents: 44721
diff changeset
   124
  /** cache for partial sharing (weak table) **/
34108
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   125
43745
562e35bc351e tuned XML.Cache parameters;
wenzelm
parents: 43520
diff changeset
   126
  class Cache(initial_size: Int = 131071, max_string: Int = 100)
34108
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   127
  {
44704
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   128
    private var table = new WeakHashMap[Any, WeakReference[Any]](initial_size)
38446
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   129
44704
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   130
    private def lookup[A](x: A): Option[A] =
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   131
    {
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   132
      val ref = table.get(x)
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   133
      if (ref == null) None
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   134
      else {
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   135
        val y = ref.asInstanceOf[WeakReference[A]].get
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   136
        if (y == null) None
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   137
        else Some(y)
38446
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   138
      }
44704
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   139
    }
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   140
    private def store[A](x: A): A =
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   141
    {
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   142
      table.put(x, new WeakReference[Any](x))
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   143
      x
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   144
    }
34108
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   145
44704
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   146
    private def trim_bytes(s: String): String = new String(s.toCharArray)
38869
wenzelm
parents: 38844
diff changeset
   147
51663
098f3cf6c809 tuned signature;
wenzelm
parents: 51223
diff changeset
   148
    private def cache_string(x: String): String =
44704
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   149
      lookup(x) match {
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   150
        case Some(y) => y
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   151
        case None =>
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   152
          val z = trim_bytes(x)
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   153
          if (z.length > max_string) z else store(z)
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   154
      }
51663
098f3cf6c809 tuned signature;
wenzelm
parents: 51223
diff changeset
   155
    private def cache_props(x: Properties.T): Properties.T =
44704
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   156
      if (x.isEmpty) x
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   157
      else
34133
wenzelm
parents: 34119
diff changeset
   158
        lookup(x) match {
wenzelm
parents: 34119
diff changeset
   159
          case Some(y) => y
51663
098f3cf6c809 tuned signature;
wenzelm
parents: 51223
diff changeset
   160
          case None => store(x.map(p => (trim_bytes(p._1).intern, cache_string(p._2))))
34133
wenzelm
parents: 34119
diff changeset
   161
        }
51663
098f3cf6c809 tuned signature;
wenzelm
parents: 51223
diff changeset
   162
    private def cache_markup(x: Markup): Markup =
44704
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   163
      lookup(x) match {
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   164
        case Some(y) => y
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   165
        case None =>
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   166
          x match {
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   167
            case Markup(name, props) =>
51663
098f3cf6c809 tuned signature;
wenzelm
parents: 51223
diff changeset
   168
              store(Markup(cache_string(name), cache_props(props)))
44704
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   169
          }
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   170
      }
51663
098f3cf6c809 tuned signature;
wenzelm
parents: 51223
diff changeset
   171
    private def cache_tree(x: XML.Tree): XML.Tree =
44704
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   172
      lookup(x) match {
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   173
        case Some(y) => y
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   174
        case None =>
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   175
          x match {
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   176
            case XML.Elem(markup, body) =>
51663
098f3cf6c809 tuned signature;
wenzelm
parents: 51223
diff changeset
   177
              store(XML.Elem(cache_markup(markup), cache_body(body)))
098f3cf6c809 tuned signature;
wenzelm
parents: 51223
diff changeset
   178
            case XML.Text(text) => store(XML.Text(cache_string(text)))
44704
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   179
          }
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   180
      }
51663
098f3cf6c809 tuned signature;
wenzelm
parents: 51223
diff changeset
   181
    private def cache_body(x: XML.Body): XML.Body =
44704
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   182
      if (x.isEmpty) x
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   183
      else
34133
wenzelm
parents: 34119
diff changeset
   184
        lookup(x) match {
wenzelm
parents: 34119
diff changeset
   185
          case Some(y) => y
51663
098f3cf6c809 tuned signature;
wenzelm
parents: 51223
diff changeset
   186
          case None => x.map(cache_tree(_))
34133
wenzelm
parents: 34119
diff changeset
   187
        }
38446
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   188
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   189
    // main methods
51663
098f3cf6c809 tuned signature;
wenzelm
parents: 51223
diff changeset
   190
    def string(x: String): String = synchronized { cache_string(x) }
098f3cf6c809 tuned signature;
wenzelm
parents: 51223
diff changeset
   191
    def props(x: Properties.T): Properties.T = synchronized { cache_props(x) }
098f3cf6c809 tuned signature;
wenzelm
parents: 51223
diff changeset
   192
    def markup(x: Markup): Markup = synchronized { cache_markup(x) }
098f3cf6c809 tuned signature;
wenzelm
parents: 51223
diff changeset
   193
    def tree(x: XML.Tree): XML.Tree = synchronized { cache_tree(x) }
098f3cf6c809 tuned signature;
wenzelm
parents: 51223
diff changeset
   194
    def body(x: XML.Body): XML.Body = synchronized { cache_body(x) }
098f3cf6c809 tuned signature;
wenzelm
parents: 51223
diff changeset
   195
    def elem(x: XML.Elem): XML.Elem = synchronized { cache_tree(x).asInstanceOf[XML.Elem] }
34108
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   196
  }
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   197
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   198
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   199
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   200
  /** XML as data representation language **/
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   201
51987
7d8e0e3c553b tuned signature;
wenzelm
parents: 51663
diff changeset
   202
  abstract class Error(s: String) extends Exception(s)
7d8e0e3c553b tuned signature;
wenzelm
parents: 51663
diff changeset
   203
  class XML_Atom(s: String) extends Error(s)
7d8e0e3c553b tuned signature;
wenzelm
parents: 51663
diff changeset
   204
  class XML_Body(body: XML.Body) extends Error("")
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   205
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   206
  object Encode
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   207
  {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   208
    type T[A] = A => XML.Body
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   209
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   210
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   211
    /* atomic values */
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   212
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   213
    def long_atom(i: Long): String = i.toString
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   214
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   215
    def int_atom(i: Int): String = i.toString
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   216
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   217
    def bool_atom(b: Boolean): String = if (b) "1" else "0"
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   218
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   219
    def unit_atom(u: Unit) = ""
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   220
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   221
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   222
    /* structural nodes */
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   223
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   224
    private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   225
43781
d43e5f79bdc2 retain some terminology of "XML attributes";
wenzelm
parents: 43780
diff changeset
   226
    private def vector(xs: List[String]): XML.Attributes =
46839
f7232c078fa5 simplified -- plain map_index is sufficient (pointed out by Enrico Tassi);
wenzelm
parents: 45673
diff changeset
   227
      xs.zipWithIndex.map({ case (x, i) => (int_atom(i), x) })
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   228
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   229
    private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree =
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   230
      XML.Elem(Markup(int_atom(tag), vector(data._1)), data._2)
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   231
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   232
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   233
    /* representation of standard types */
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   234
43780
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43778
diff changeset
   235
    val properties: T[Properties.T] =
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   236
      (props => List(XML.Elem(Markup(":", props), Nil)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   237
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   238
    val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   239
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   240
    val long: T[Long] = (x => string(long_atom(x)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   241
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   242
    val int: T[Int] = (x => string(int_atom(x)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   243
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   244
    val bool: T[Boolean] = (x => string(bool_atom(x)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   245
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   246
    val unit: T[Unit] = (x => string(unit_atom(x)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   247
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   248
    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   249
      (x => List(node(f(x._1)), node(g(x._2))))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   250
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   251
    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   252
      (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3))))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   253
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   254
    def list[A](f: T[A]): T[List[A]] =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   255
      (xs => xs.map((x: A) => node(f(x))))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   256
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   257
    def option[A](f: T[A]): T[Option[A]] =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   258
    {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   259
      case None => Nil
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   260
      case Some(x) => List(node(f(x)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   261
    }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   262
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   263
    def variant[A](fs: List[PartialFunction[A, (List[String], XML.Body)]]): T[A] =
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   264
    {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   265
      case x =>
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   266
        val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   267
        List(tagged(tag, f(x)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   268
    }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   269
  }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   270
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   271
  object Decode
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   272
  {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   273
    type T[A] = XML.Body => A
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   274
    type V[A] = (List[String], XML.Body) => A
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   275
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   276
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   277
    /* atomic values */
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   278
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   279
    def long_atom(s: String): Long =
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   280
      try { java.lang.Long.parseLong(s) }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   281
      catch { case e: NumberFormatException => throw new XML_Atom(s) }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   282
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   283
    def int_atom(s: String): Int =
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   284
      try { Integer.parseInt(s) }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   285
      catch { case e: NumberFormatException => throw new XML_Atom(s) }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   286
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   287
    def bool_atom(s: String): Boolean =
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   288
      if (s == "1") true
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   289
      else if (s == "0") false
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   290
      else throw new XML_Atom(s)
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   291
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   292
    def unit_atom(s: String): Unit =
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   293
      if (s == "") () else throw new XML_Atom(s)
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   294
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   295
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   296
    /* structural nodes */
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   297
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   298
    private def node(t: XML.Tree): XML.Body =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   299
      t match {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   300
        case XML.Elem(Markup(":", Nil), ts) => ts
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   301
        case _ => throw new XML_Body(List(t))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   302
      }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   303
43781
d43e5f79bdc2 retain some terminology of "XML attributes";
wenzelm
parents: 43780
diff changeset
   304
    private def vector(atts: XML.Attributes): List[String] =
46839
f7232c078fa5 simplified -- plain map_index is sufficient (pointed out by Enrico Tassi);
wenzelm
parents: 45673
diff changeset
   305
      atts.iterator.zipWithIndex.map(
f7232c078fa5 simplified -- plain map_index is sufficient (pointed out by Enrico Tassi);
wenzelm
parents: 45673
diff changeset
   306
        { case ((a, x), i) => if (int_atom(a) == i) x else throw new XML_Atom(a) }).toList
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   307
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   308
    private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) =
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   309
      t match {
43781
d43e5f79bdc2 retain some terminology of "XML attributes";
wenzelm
parents: 43780
diff changeset
   310
        case XML.Elem(Markup(name, atts), ts) => (int_atom(name), (vector(atts), ts))
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   311
        case _ => throw new XML_Body(List(t))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   312
      }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   313
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   314
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   315
    /* representation of standard types */
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   316
43780
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43778
diff changeset
   317
    val properties: T[Properties.T] =
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   318
    {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   319
      case List(XML.Elem(Markup(":", props), Nil)) => props
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   320
      case ts => throw new XML_Body(ts)
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   321
    }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   322
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   323
    val string: T[String] =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   324
    {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   325
      case Nil => ""
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   326
      case List(XML.Text(s)) => s
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   327
      case ts => throw new XML_Body(ts)
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   328
    }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   329
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   330
    val long: T[Long] = (x => long_atom(string(x)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   331
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   332
    val int: T[Int] = (x => int_atom(string(x)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   333
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   334
    val bool: T[Boolean] = (x => bool_atom(string(x)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   335
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   336
    val unit: T[Unit] = (x => unit_atom(string(x)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   337
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   338
    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   339
    {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   340
      case List(t1, t2) => (f(node(t1)), g(node(t2)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   341
      case ts => throw new XML_Body(ts)
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   342
    }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   343
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   344
    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   345
    {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   346
      case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   347
      case ts => throw new XML_Body(ts)
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   348
    }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   349
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   350
    def list[A](f: T[A]): T[List[A]] =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   351
      (ts => ts.map(t => f(node(t))))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   352
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   353
    def option[A](f: T[A]): T[Option[A]] =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   354
    {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   355
      case Nil => None
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   356
      case List(t) => Some(f(node(t)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   357
      case ts => throw new XML_Body(ts)
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   358
    }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   359
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   360
    def variant[A](fs: List[V[A]]): T[A] =
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   361
    {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   362
      case List(t) =>
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   363
        val (tag, (xs, ts)) = tagged(t)
43768
d52ab827d62b more precise exceptions;
wenzelm
parents: 43767
diff changeset
   364
        val f =
d52ab827d62b more precise exceptions;
wenzelm
parents: 43767
diff changeset
   365
          try { fs(tag) }
d52ab827d62b more precise exceptions;
wenzelm
parents: 43767
diff changeset
   366
          catch { case _: IndexOutOfBoundsException => throw new XML_Body(List(t)) }
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   367
        f(xs, ts)
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   368
      case ts => throw new XML_Body(ts)
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   369
    }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   370
  }
27931
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
   371
}