src/Pure/PIDE/xml.scala
author wenzelm
Tue, 29 Nov 2011 21:50:00 +0100
changeset 45674 eb65c9d17e2f
parent 45673 cd41e3903fbf
child 46839 f7232c078fa5
permissions -rw-r--r--
clarified Time vs. Timing;
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
43520
cec9b95fa35d explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents: 38869
diff changeset
    10
import java.lang.System
34108
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
    11
import java.util.WeakHashMap
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
    12
import java.lang.ref.WeakReference
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
    13
import javax.xml.parsers.DocumentBuilderFactory
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
    14
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
    15
import scala.collection.mutable
38446
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
    16
27947
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
    17
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    18
object XML
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    19
{
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
    20
  /** XML trees **/
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
    21
27947
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
    22
  /* datatype representation */
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
    23
43780
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43778
diff changeset
    24
  type Attributes = Properties.T
27931
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
    25
38268
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    26
  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
    27
  case class Elem(markup: Markup, body: List[Tree]) extends Tree
29204
wenzelm
parents: 29203
diff changeset
    28
  case class Text(content: String) extends Tree
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    29
38230
ed147003de4b simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents: 36817
diff changeset
    30
  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
    31
  def elem(name: String) = Elem(Markup(name, Nil), Nil)
33999
d3b200894e21 added auxiliary constructors;
wenzelm
parents: 33953
diff changeset
    32
38267
e50c283dd125 type XML.Body as basic data representation language (Scala version);
wenzelm
parents: 38263
diff changeset
    33
  type Body = List[Tree]
e50c283dd125 type XML.Body as basic data representation language (Scala version);
wenzelm
parents: 38263
diff changeset
    34
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    35
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    36
  /* string representation */
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    37
38268
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    38
  def string_of_body(body: Body): String =
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    39
  {
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    40
    val s = new StringBuilder
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    41
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    42
    def text(txt: String) {
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    43
      if (txt == null) s ++= txt
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    44
      else {
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    45
        for (c <- txt.iterator) c match {
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    46
          case '<' => s ++= "&lt;"
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    47
          case '>' => s ++= "&gt;"
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    48
          case '&' => s ++= "&amp;"
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    49
          case '"' => s ++= "&quot;"
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    50
          case '\'' => s ++= "&apos;"
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    51
          case _ => s += c
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    52
        }
34005
ada5098506af toString: more robust handling of null;
wenzelm
parents: 33999
diff changeset
    53
      }
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    54
    }
38268
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    55
    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
    56
    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
    57
    def tree(t: Tree): Unit =
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    58
      t match {
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    59
        case Elem(markup, Nil) =>
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    60
          s ++= "<"; elem(markup); s ++= "/>"
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    61
        case Elem(markup, ts) =>
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    62
          s ++= "<"; elem(markup); s ++= ">"
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    63
          ts.foreach(tree)
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    64
          s ++= "</"; s ++= markup.name; s ++= ">"
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    65
        case Text(txt) => text(txt)
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    66
      }
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    67
    body.foreach(tree)
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    68
    s.toString
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    69
  }
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    70
38268
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    71
  def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
27941
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    72
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    73
38484
9c1fde4e2487 tuned XML.content: Stream based iteration is supposed to be declarative *and* efficient;
wenzelm
parents: 38446
diff changeset
    74
  /* text content */
27941
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    75
38484
9c1fde4e2487 tuned XML.content: Stream based iteration is supposed to be declarative *and* efficient;
wenzelm
parents: 38446
diff changeset
    76
  def content_stream(tree: Tree): Stream[String] =
9c1fde4e2487 tuned XML.content: Stream based iteration is supposed to be declarative *and* efficient;
wenzelm
parents: 38446
diff changeset
    77
    tree match {
43747
74a9e9c8d5e8 tuned signature;
wenzelm
parents: 43745
diff changeset
    78
      case Elem(_, body) => content_stream(body)
38484
9c1fde4e2487 tuned XML.content: Stream based iteration is supposed to be declarative *and* efficient;
wenzelm
parents: 38446
diff changeset
    79
      case Text(content) => Stream(content)
27941
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    80
    }
43747
74a9e9c8d5e8 tuned signature;
wenzelm
parents: 43745
diff changeset
    81
  def content_stream(body: Body): Stream[String] =
74a9e9c8d5e8 tuned signature;
wenzelm
parents: 43745
diff changeset
    82
    body.toStream.flatten(content_stream(_))
27941
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    83
38484
9c1fde4e2487 tuned XML.content: Stream based iteration is supposed to be declarative *and* efficient;
wenzelm
parents: 38446
diff changeset
    84
  def content(tree: Tree): Iterator[String] = content_stream(tree).iterator
43747
74a9e9c8d5e8 tuned signature;
wenzelm
parents: 43745
diff changeset
    85
  def content(body: Body): Iterator[String] = content_stream(body).iterator
27941
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    86
27947
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
    87
44808
05b8997899a2 XML.cache for partial sharing (strings only);
wenzelm
parents: 44721
diff changeset
    88
05b8997899a2 XML.cache for partial sharing (strings only);
wenzelm
parents: 44721
diff changeset
    89
  /** cache for partial sharing (weak table) **/
34108
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
    90
43745
562e35bc351e tuned XML.Cache parameters;
wenzelm
parents: 43520
diff changeset
    91
  class Cache(initial_size: Int = 131071, max_string: Int = 100)
34108
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
    92
  {
44704
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
    93
    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
    94
44704
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
    95
    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
    96
    {
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
    97
      val ref = table.get(x)
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
    98
      if (ref == null) None
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
    99
      else {
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   100
        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
   101
        if (y == null) None
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   102
        else Some(y)
38446
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   103
      }
44704
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   104
    }
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   105
    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
   106
    {
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   107
      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
   108
      x
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   109
    }
34108
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   110
44704
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   111
    private def trim_bytes(s: String): String = new String(s.toCharArray)
38869
wenzelm
parents: 38844
diff changeset
   112
44704
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   113
    private def _cache_string(x: String): String =
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   114
      lookup(x) match {
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   115
        case Some(y) => y
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   116
        case None =>
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   117
          val z = trim_bytes(x)
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   118
          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
   119
      }
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   120
    private def _cache_props(x: Properties.T): Properties.T =
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   121
      if (x.isEmpty) x
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   122
      else
34133
wenzelm
parents: 34119
diff changeset
   123
        lookup(x) match {
wenzelm
parents: 34119
diff changeset
   124
          case Some(y) => y
44704
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   125
          case None => store(x.map(p => (trim_bytes(p._1).intern, _cache_string(p._2))))
34133
wenzelm
parents: 34119
diff changeset
   126
        }
44704
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   127
    private def _cache_markup(x: Markup): Markup =
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   128
      lookup(x) match {
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   129
        case Some(y) => y
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   130
        case None =>
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   131
          x match {
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   132
            case Markup(name, props) =>
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   133
              store(Markup(_cache_string(name), _cache_props(props)))
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   134
          }
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   135
      }
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   136
    private def _cache_tree(x: XML.Tree): XML.Tree =
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   137
      lookup(x) match {
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   138
        case Some(y) => y
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   139
        case None =>
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   140
          x match {
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   141
            case XML.Elem(markup, body) =>
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   142
              store(XML.Elem(_cache_markup(markup), _cache_body(body)))
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   143
            case XML.Text(text) => store(XML.Text(_cache_string(text)))
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   144
          }
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   145
      }
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   146
    private def _cache_body(x: XML.Body): XML.Body =
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   147
      if (x.isEmpty) x
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   148
      else
34133
wenzelm
parents: 34119
diff changeset
   149
        lookup(x) match {
wenzelm
parents: 34119
diff changeset
   150
          case Some(y) => y
44704
528d635ef6f0 synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
wenzelm
parents: 44698
diff changeset
   151
          case None => x.map(_cache_tree(_))
34133
wenzelm
parents: 34119
diff changeset
   152
        }
38446
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   153
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   154
    // main methods
44705
089fcaf94c00 simplified signatures;
wenzelm
parents: 44704
diff changeset
   155
    def cache_string(x: String): String = synchronized { _cache_string(x) }
089fcaf94c00 simplified signatures;
wenzelm
parents: 44704
diff changeset
   156
    def cache_markup(x: Markup): Markup = synchronized { _cache_markup(x) }
089fcaf94c00 simplified signatures;
wenzelm
parents: 44704
diff changeset
   157
    def cache_tree(x: XML.Tree): XML.Tree = synchronized { _cache_tree(x) }
089fcaf94c00 simplified signatures;
wenzelm
parents: 44704
diff changeset
   158
    def cache_body(x: XML.Body): XML.Body = synchronized { _cache_body(x) }
34108
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   159
  }
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   160
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   161
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   162
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   163
  /** document object model (W3C DOM) **/
27948
2638b611d3ce renamed DOM to document, add xml version and optional stylesheets;
wenzelm
parents: 27947
diff changeset
   164
34871
e596a0b71f3c incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
wenzelm
parents: 34133
diff changeset
   165
  def get_data(node: org.w3c.dom.Node): Option[XML.Tree] =
38231
968844caaff9 simplified some Markup;
wenzelm
parents: 38230
diff changeset
   166
    node.getUserData(Markup.Data.name) match {
34047
2af94d45597f added get_data;
wenzelm
parents: 34046
diff changeset
   167
      case tree: XML.Tree => Some(tree)
2af94d45597f added get_data;
wenzelm
parents: 34046
diff changeset
   168
      case _ => None
2af94d45597f added get_data;
wenzelm
parents: 34046
diff changeset
   169
    }
2af94d45597f added get_data;
wenzelm
parents: 34046
diff changeset
   170
34871
e596a0b71f3c incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
wenzelm
parents: 34133
diff changeset
   171
  def document_node(doc: org.w3c.dom.Document, tree: Tree): org.w3c.dom.Node =
33953
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   172
  {
34871
e596a0b71f3c incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
wenzelm
parents: 34133
diff changeset
   173
    def DOM(tr: Tree): org.w3c.dom.Node = tr match {
38231
968844caaff9 simplified some Markup;
wenzelm
parents: 38230
diff changeset
   174
      case Elem(Markup.Data, List(data, t)) =>
34046
8e743ca417b9 sealed XML.Tree;
wenzelm
parents: 34005
diff changeset
   175
        val node = DOM(t)
38231
968844caaff9 simplified some Markup;
wenzelm
parents: 38230
diff changeset
   176
        node.setUserData(Markup.Data.name, data, null)
34046
8e743ca417b9 sealed XML.Tree;
wenzelm
parents: 34005
diff changeset
   177
        node
38230
ed147003de4b simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents: 36817
diff changeset
   178
      case Elem(Markup(name, atts), ts) =>
38231
968844caaff9 simplified some Markup;
wenzelm
parents: 38230
diff changeset
   179
        if (name == Markup.Data.name)
34046
8e743ca417b9 sealed XML.Tree;
wenzelm
parents: 34005
diff changeset
   180
          error("Malformed data element: " + tr.toString)
27947
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   181
        val node = doc.createElement(name)
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   182
        for ((name, value) <- atts) node.setAttribute(name, value)
27952
wenzelm
parents: 27948
diff changeset
   183
        for (t <- ts) node.appendChild(DOM(t))
27947
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   184
        node
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   185
      case Text(txt) => doc.createTextNode(txt)
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   186
    }
33953
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   187
    DOM(tree)
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   188
  }
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   189
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   190
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   191
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   192
  /** XML as data representation language **/
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   193
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   194
  class XML_Atom(s: String) extends Exception(s)
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   195
  class XML_Body(body: XML.Body) extends Exception
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   196
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   197
  object Encode
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   198
  {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   199
    type T[A] = A => XML.Body
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   200
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   201
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   202
    /* atomic values */
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   203
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   204
    def long_atom(i: Long): String = i.toString
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   205
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   206
    def int_atom(i: Int): String = i.toString
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   207
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   208
    def bool_atom(b: Boolean): String = if (b) "1" else "0"
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   209
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   210
    def unit_atom(u: Unit) = ""
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   211
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   212
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   213
    /* structural nodes */
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   214
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   215
    private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   216
43781
d43e5f79bdc2 retain some terminology of "XML attributes";
wenzelm
parents: 43780
diff changeset
   217
    private def vector(xs: List[String]): XML.Attributes =
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   218
      xs.zipWithIndex.map(p => (int_atom(p._2), p._1))
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   219
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   220
    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
   221
      XML.Elem(Markup(int_atom(tag), vector(data._1)), data._2)
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   222
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   223
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   224
    /* representation of standard types */
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   225
43780
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43778
diff changeset
   226
    val properties: T[Properties.T] =
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   227
      (props => List(XML.Elem(Markup(":", props), Nil)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   228
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   229
    val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   230
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   231
    val long: T[Long] = (x => string(long_atom(x)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   232
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   233
    val int: T[Int] = (x => string(int_atom(x)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   234
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   235
    val bool: T[Boolean] = (x => string(bool_atom(x)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   236
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   237
    val unit: T[Unit] = (x => string(unit_atom(x)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   238
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   239
    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   240
      (x => List(node(f(x._1)), node(g(x._2))))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   241
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   242
    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
   243
      (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3))))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   244
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   245
    def list[A](f: T[A]): T[List[A]] =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   246
      (xs => xs.map((x: A) => node(f(x))))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   247
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   248
    def option[A](f: T[A]): T[Option[A]] =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   249
    {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   250
      case None => Nil
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   251
      case Some(x) => List(node(f(x)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   252
    }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   253
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   254
    def variant[A](fs: List[PartialFunction[A, (List[String], XML.Body)]]): T[A] =
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   255
    {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   256
      case x =>
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   257
        val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   258
        List(tagged(tag, f(x)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   259
    }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   260
  }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   261
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   262
  object Decode
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   263
  {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   264
    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
   265
    type V[A] = (List[String], XML.Body) => A
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   266
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   267
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   268
    /* atomic values */
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   269
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   270
    def long_atom(s: String): Long =
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   271
      try { java.lang.Long.parseLong(s) }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   272
      catch { case e: NumberFormatException => throw new XML_Atom(s) }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   273
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
    def int_atom(s: String): Int =
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   275
      try { Integer.parseInt(s) }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   276
      catch { case e: NumberFormatException => throw new XML_Atom(s) }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   277
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   278
    def bool_atom(s: String): Boolean =
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   279
      if (s == "1") true
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   280
      else if (s == "0") false
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   281
      else 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 unit_atom(s: String): Unit =
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   284
      if (s == "") () else throw new XML_Atom(s)
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   285
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   286
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   287
    /* structural nodes */
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   288
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   289
    private def node(t: XML.Tree): XML.Body =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   290
      t match {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   291
        case XML.Elem(Markup(":", Nil), ts) => ts
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   292
        case _ => throw new XML_Body(List(t))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   293
      }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   294
43781
d43e5f79bdc2 retain some terminology of "XML attributes";
wenzelm
parents: 43780
diff changeset
   295
    private def vector(atts: XML.Attributes): List[String] =
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   296
    {
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   297
      val xs = new mutable.ListBuffer[String]
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   298
      var i = 0
43781
d43e5f79bdc2 retain some terminology of "XML attributes";
wenzelm
parents: 43780
diff changeset
   299
      for ((a, x) <- atts) {
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   300
        if (int_atom(a) == i) { xs += x; i = i + 1 }
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   301
        else throw new XML_Atom(a)
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   302
      }
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   303
      xs.toList
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   304
    }
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   305
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   306
    private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) =
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   307
      t match {
43781
d43e5f79bdc2 retain some terminology of "XML attributes";
wenzelm
parents: 43780
diff changeset
   308
        case XML.Elem(Markup(name, atts), ts) => (int_atom(name), (vector(atts), ts))
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   309
        case _ => throw new XML_Body(List(t))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   310
      }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   311
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   312
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   313
    /* representation of standard types */
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   314
43780
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43778
diff changeset
   315
    val properties: T[Properties.T] =
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   316
    {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   317
      case List(XML.Elem(Markup(":", props), Nil)) => props
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   318
      case ts => throw new XML_Body(ts)
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   319
    }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   320
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   321
    val string: T[String] =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   322
    {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   323
      case Nil => ""
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   324
      case List(XML.Text(s)) => s
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   325
      case ts => throw new XML_Body(ts)
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   326
    }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   327
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   328
    val long: T[Long] = (x => long_atom(string(x)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   329
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   330
    val int: T[Int] = (x => int_atom(string(x)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   331
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   332
    val bool: T[Boolean] = (x => bool_atom(string(x)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   333
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   334
    val unit: T[Unit] = (x => unit_atom(string(x)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   335
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   336
    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   337
    {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   338
      case List(t1, t2) => (f(node(t1)), g(node(t2)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   339
      case ts => throw new XML_Body(ts)
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   340
    }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   341
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   342
    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
   343
    {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   344
      case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   345
      case ts => throw new XML_Body(ts)
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   346
    }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   347
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   348
    def list[A](f: T[A]): T[List[A]] =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   349
      (ts => ts.map(t => f(node(t))))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   350
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   351
    def option[A](f: T[A]): T[Option[A]] =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   352
    {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   353
      case Nil => None
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   354
      case List(t) => Some(f(node(t)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   355
      case ts => throw new XML_Body(ts)
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   356
    }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   357
43778
ce9189450447 more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents: 43768
diff changeset
   358
    def variant[A](fs: List[V[A]]): T[A] =
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   359
    {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   360
      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
   361
        val (tag, (xs, ts)) = tagged(t)
43768
d52ab827d62b more precise exceptions;
wenzelm
parents: 43767
diff changeset
   362
        val f =
d52ab827d62b more precise exceptions;
wenzelm
parents: 43767
diff changeset
   363
          try { fs(tag) }
d52ab827d62b more precise exceptions;
wenzelm
parents: 43767
diff changeset
   364
          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
   365
        f(xs, ts)
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   366
      case ts => throw new XML_Body(ts)
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   367
    }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   368
  }
27931
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
   369
}