src/Pure/General/xml.scala
author wenzelm
Tue, 12 Jul 2011 10:44:30 +0200
changeset 43767 e0219ef7f84c
parent 43747 74a9e9c8d5e8
child 43768 d52ab827d62b
permissions -rw-r--r--
tuned XML modules;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27931
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/xml.scala
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
     3
27947
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
     4
Simple XML tree values.
27931
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
     5
*/
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
     6
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
     7
package isabelle
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
     8
43520
cec9b95fa35d explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents: 38869
diff changeset
     9
import java.lang.System
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
38446
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
    14
import scala.actors.Actor._
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
    15
27947
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
    16
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    17
object XML
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    18
{
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
    19
  /** XML trees **/
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
    20
27947
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
    21
  /* datatype representation */
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
    22
27931
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
    23
  type Attributes = List[(String, String)]
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
    24
38268
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    25
  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
    26
  case class Elem(markup: Markup, body: List[Tree]) extends Tree
29204
wenzelm
parents: 29203
diff changeset
    27
  case class Text(content: String) extends Tree
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    28
38230
ed147003de4b simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents: 36817
diff changeset
    29
  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
    30
  def elem(name: String) = Elem(Markup(name, Nil), Nil)
33999
d3b200894e21 added auxiliary constructors;
wenzelm
parents: 33953
diff changeset
    31
38267
e50c283dd125 type XML.Body as basic data representation language (Scala version);
wenzelm
parents: 38263
diff changeset
    32
  type Body = List[Tree]
e50c283dd125 type XML.Body as basic data representation language (Scala version);
wenzelm
parents: 38263
diff changeset
    33
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    34
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    35
  /* string representation */
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    36
38268
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    37
  def string_of_body(body: Body): String =
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    38
  {
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    39
    val s = new StringBuilder
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    40
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    41
    def text(txt: String) {
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    42
      if (txt == null) s ++= txt
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    43
      else {
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    44
        for (c <- txt.iterator) c match {
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    45
          case '<' => s ++= "&lt;"
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    46
          case '>' => s ++= "&gt;"
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    47
          case '&' => s ++= "&amp;"
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    48
          case '"' => s ++= "&quot;"
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    49
          case '\'' => s ++= "&apos;"
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    50
          case _ => s += c
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    51
        }
34005
ada5098506af toString: more robust handling of null;
wenzelm
parents: 33999
diff changeset
    52
      }
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    53
    }
38268
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    54
    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
    55
    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
    56
    def tree(t: Tree): Unit =
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    57
      t match {
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    58
        case Elem(markup, Nil) =>
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    59
          s ++= "<"; elem(markup); s ++= "/>"
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    60
        case Elem(markup, ts) =>
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    61
          s ++= "<"; elem(markup); s ++= ">"
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    62
          ts.foreach(tree)
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    63
          s ++= "</"; s ++= markup.name; s ++= ">"
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    64
        case Text(txt) => text(txt)
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    65
      }
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    66
    body.foreach(tree)
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    67
    s.toString
29203
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    68
  }
0c4effb73518 override toString method;
wenzelm
parents: 29140
diff changeset
    69
38268
beb86b805590 more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents: 38267
diff changeset
    70
  def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
27941
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    71
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    72
38484
9c1fde4e2487 tuned XML.content: Stream based iteration is supposed to be declarative *and* efficient;
wenzelm
parents: 38446
diff changeset
    73
  /* text content */
27941
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    74
38484
9c1fde4e2487 tuned XML.content: Stream based iteration is supposed to be declarative *and* efficient;
wenzelm
parents: 38446
diff changeset
    75
  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
    76
    tree match {
43747
74a9e9c8d5e8 tuned signature;
wenzelm
parents: 43745
diff changeset
    77
      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
    78
      case Text(content) => Stream(content)
27941
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    79
    }
43747
74a9e9c8d5e8 tuned signature;
wenzelm
parents: 43745
diff changeset
    80
  def content_stream(body: Body): Stream[String] =
74a9e9c8d5e8 tuned signature;
wenzelm
parents: 43745
diff changeset
    81
    body.toStream.flatten(content_stream(_))
27941
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    82
38484
9c1fde4e2487 tuned XML.content: Stream based iteration is supposed to be declarative *and* efficient;
wenzelm
parents: 38446
diff changeset
    83
  def content(tree: Tree): Iterator[String] = content_stream(tree).iterator
43747
74a9e9c8d5e8 tuned signature;
wenzelm
parents: 43745
diff changeset
    84
  def content(body: Body): Iterator[String] = content_stream(body).iterator
27941
b4656b671cce added iterator over content;
wenzelm
parents: 27931
diff changeset
    85
27947
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
    86
38446
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
    87
  /* pipe-lined cache for partial sharing */
34108
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
    88
43745
562e35bc351e tuned XML.Cache parameters;
wenzelm
parents: 43520
diff changeset
    89
  class Cache(initial_size: Int = 131071, max_string: Int = 100)
34108
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
    90
  {
38446
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
    91
    private val cache_actor = actor
34108
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
    92
    {
38446
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
    93
      val table = new WeakHashMap[Any, WeakReference[Any]](initial_size)
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
    94
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
    95
      def lookup[A](x: A): Option[A] =
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
    96
      {
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
    97
        val ref = table.get(x)
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
    98
        if (ref == null) None
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
    99
        else {
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   100
          val y = ref.asInstanceOf[WeakReference[A]].get
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   101
          if (y == null) None
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   102
          else Some(y)
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   103
        }
34108
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   104
      }
38446
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   105
      def store[A](x: A): A =
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   106
      {
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   107
        table.put(x, new WeakReference[Any](x))
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   108
        x
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   109
      }
34108
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   110
38869
wenzelm
parents: 38844
diff changeset
   111
      def trim_bytes(s: String): String = new String(s.toCharArray)
wenzelm
parents: 38844
diff changeset
   112
38446
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   113
      def cache_string(x: String): String =
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   114
        lookup(x) match {
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   115
          case Some(y) => y
43745
562e35bc351e tuned XML.Cache parameters;
wenzelm
parents: 43520
diff changeset
   116
          case None =>
562e35bc351e tuned XML.Cache parameters;
wenzelm
parents: 43520
diff changeset
   117
            val z = trim_bytes(x)
562e35bc351e tuned XML.Cache parameters;
wenzelm
parents: 43520
diff changeset
   118
            if (z.length > max_string) z else store(z)
38446
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   119
        }
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   120
      def cache_props(x: List[(String, String)]): List[(String, String)] =
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   121
        if (x.isEmpty) x
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   122
        else
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   123
          lookup(x) match {
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   124
            case Some(y) => y
38869
wenzelm
parents: 38844
diff changeset
   125
            case None => store(x.map(p => (trim_bytes(p._1).intern, cache_string(p._2))))
38446
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   126
          }
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   127
      def cache_markup(x: Markup): Markup =
34133
wenzelm
parents: 34119
diff changeset
   128
        lookup(x) match {
wenzelm
parents: 34119
diff changeset
   129
          case Some(y) => y
38446
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   130
          case None =>
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   131
            x match {
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   132
              case Markup(name, props) =>
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   133
                store(Markup(cache_string(name), cache_props(props)))
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   134
            }
34133
wenzelm
parents: 34119
diff changeset
   135
        }
38446
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   136
      def cache_tree(x: XML.Tree): XML.Tree =
34133
wenzelm
parents: 34119
diff changeset
   137
        lookup(x) match {
wenzelm
parents: 34119
diff changeset
   138
          case Some(y) => y
38446
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   139
          case None =>
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   140
            x match {
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   141
              case XML.Elem(markup, body) =>
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   142
                store(XML.Elem(cache_markup(markup), cache_body(body)))
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   143
              case XML.Text(text) => store(XML.Text(cache_string(text)))
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   144
            }
34133
wenzelm
parents: 34119
diff changeset
   145
        }
38446
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   146
      def cache_body(x: XML.Body): XML.Body =
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   147
        if (x.isEmpty) x
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   148
        else
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   149
          lookup(x) match {
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   150
            case Some(y) => y
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   151
            case None => x.map(cache_tree(_))
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   152
          }
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 loop
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   155
      loop {
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   156
        react {
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   157
          case Cache_String(x, f) => f(cache_string(x))
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   158
          case Cache_Markup(x, f) => f(cache_markup(x))
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   159
          case Cache_Tree(x, f) => f(cache_tree(x))
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   160
          case Cache_Body(x, f) => f(cache_body(x))
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   161
          case bad => System.err.println("XML.cache_actor: ignoring bad input " + bad)
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   162
        }
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   163
      }
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   164
    }
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   165
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   166
    private case class Cache_String(x: String, f: String => Unit)
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   167
    private case class Cache_Markup(x: Markup, f: Markup => Unit)
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   168
    private case class Cache_Tree(x: XML.Tree, f: XML.Tree => Unit)
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   169
    private case class Cache_Body(x: XML.Body, f: XML.Body => Unit)
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   170
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   171
    // main methods
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   172
    def cache_string(x: String)(f: String => Unit) { cache_actor ! Cache_String(x, f) }
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   173
    def cache_markup(x: Markup)(f: Markup => Unit) { cache_actor ! Cache_Markup(x, f) }
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   174
    def cache_tree(x: XML.Tree)(f: XML.Tree => Unit) { cache_actor ! Cache_Tree(x, f) }
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38268
diff changeset
   175
    def cache_body(x: XML.Body)(f: XML.Body => Unit) { cache_actor ! Cache_Body(x, f) }
34108
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   176
  }
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   177
54d48ca8708f cache for partial sharing;
wenzelm
parents: 34047
diff changeset
   178
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   179
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   180
  /** document object model (W3C DOM) **/
27948
2638b611d3ce renamed DOM to document, add xml version and optional stylesheets;
wenzelm
parents: 27947
diff changeset
   181
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
   182
  def get_data(node: org.w3c.dom.Node): Option[XML.Tree] =
38231
968844caaff9 simplified some Markup;
wenzelm
parents: 38230
diff changeset
   183
    node.getUserData(Markup.Data.name) match {
34047
2af94d45597f added get_data;
wenzelm
parents: 34046
diff changeset
   184
      case tree: XML.Tree => Some(tree)
2af94d45597f added get_data;
wenzelm
parents: 34046
diff changeset
   185
      case _ => None
2af94d45597f added get_data;
wenzelm
parents: 34046
diff changeset
   186
    }
2af94d45597f added get_data;
wenzelm
parents: 34046
diff changeset
   187
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
   188
  def document_node(doc: org.w3c.dom.Document, tree: Tree): org.w3c.dom.Node =
33953
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   189
  {
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
   190
    def DOM(tr: Tree): org.w3c.dom.Node = tr match {
38231
968844caaff9 simplified some Markup;
wenzelm
parents: 38230
diff changeset
   191
      case Elem(Markup.Data, List(data, t)) =>
34046
8e743ca417b9 sealed XML.Tree;
wenzelm
parents: 34005
diff changeset
   192
        val node = DOM(t)
38231
968844caaff9 simplified some Markup;
wenzelm
parents: 38230
diff changeset
   193
        node.setUserData(Markup.Data.name, data, null)
34046
8e743ca417b9 sealed XML.Tree;
wenzelm
parents: 34005
diff changeset
   194
        node
38230
ed147003de4b simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents: 36817
diff changeset
   195
      case Elem(Markup(name, atts), ts) =>
38231
968844caaff9 simplified some Markup;
wenzelm
parents: 38230
diff changeset
   196
        if (name == Markup.Data.name)
34046
8e743ca417b9 sealed XML.Tree;
wenzelm
parents: 34005
diff changeset
   197
          error("Malformed data element: " + tr.toString)
27947
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   198
        val node = doc.createElement(name)
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   199
        for ((name, value) <- atts) node.setAttribute(name, value)
27952
wenzelm
parents: 27948
diff changeset
   200
        for (t <- ts) node.appendChild(DOM(t))
27947
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   201
        node
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   202
      case Text(txt) => doc.createTextNode(txt)
b6dc0a396857 tuned comments;
wenzelm
parents: 27942
diff changeset
   203
    }
33953
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   204
    DOM(tree)
5e865ed88313 added document_node;
wenzelm
parents: 29204
diff changeset
   205
  }
43767
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   206
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   207
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   208
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   209
  /** XML as data representation language **/
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   210
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   211
  class XML_Atom(s: String) extends Exception(s)
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   212
  class XML_Body(body: XML.Body) extends Exception
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   213
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   214
  object Encode
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   215
  {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   216
    type T[A] = A => XML.Body
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   217
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   218
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   219
    /* basic values */
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   220
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   221
    private def long_atom(i: Long): String = i.toString
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   222
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   223
    private def int_atom(i: Int): String = i.toString
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   224
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   225
    private def bool_atom(b: Boolean): String = if (b) "1" else "0"
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   226
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   227
    private def unit_atom(u: Unit) = ""
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   228
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   229
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   230
    /* structural nodes */
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   231
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   232
    private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   233
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   234
    private def tagged(tag: Int, ts: XML.Body): XML.Tree =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   235
      XML.Elem(Markup(int_atom(tag), Nil), ts)
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   236
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   237
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   238
    /* representation of standard types */
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   239
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   240
    val properties: T[List[(String, String)]] =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   241
      (props => List(XML.Elem(Markup(":", props), Nil)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   242
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   243
    val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   244
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   245
    val long: T[Long] = (x => string(long_atom(x)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   246
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   247
    val int: T[Int] = (x => string(int_atom(x)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   248
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   249
    val bool: T[Boolean] = (x => string(bool_atom(x)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   250
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   251
    val unit: T[Unit] = (x => string(unit_atom(x)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   252
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   253
    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   254
      (x => List(node(f(x._1)), node(g(x._2))))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   255
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   256
    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
   257
      (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3))))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   258
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   259
    def list[A](f: T[A]): T[List[A]] =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   260
      (xs => xs.map((x: A) => node(f(x))))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   261
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   262
    def option[A](f: T[A]): T[Option[A]] =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   263
    {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   264
      case None => Nil
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   265
      case Some(x) => List(node(f(x)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   266
    }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   267
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   268
    def variant[A](fs: List[PartialFunction[A, XML.Body]]): T[A] =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   269
    {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   270
      case x =>
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   271
        val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   272
        List(tagged(tag, f(x)))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   273
    }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   274
  }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   275
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   276
  object Decode
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   277
  {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   278
    type T[A] = XML.Body => A
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   279
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   280
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   281
     /* basic values */
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   282
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   283
    private def long_atom(s: String): Long =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   284
      try { java.lang.Long.parseLong(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
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   287
    private def int_atom(s: String): Int =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   288
      try { Integer.parseInt(s) }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   289
      catch { case e: NumberFormatException => throw new XML_Atom(s) }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   290
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   291
    private def bool_atom(s: String): Boolean =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   292
      if (s == "1") true
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   293
      else if (s == "0") false
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   294
      else throw new XML_Atom(s)
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   295
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   296
    private def unit_atom(s: String): Unit =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   297
      if (s == "") () else throw new XML_Atom(s)
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   298
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   299
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   300
    /* structural nodes */
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   301
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   302
    private def node(t: XML.Tree): XML.Body =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   303
      t match {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   304
        case XML.Elem(Markup(":", Nil), ts) => ts
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   305
        case _ => throw new XML_Body(List(t))
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   306
      }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   307
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   308
    private def tagged(t: XML.Tree): (Int, XML.Body) =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   309
      t match {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   310
        case XML.Elem(Markup(s, Nil), ts) => (int_atom(s), ts)
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
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   317
    val properties: T[List[(String, String)]] =
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
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   360
    def variant[A](fs: List[T[A]]): T[A] =
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   361
    {
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   362
      case List(t) =>
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   363
        val (tag, ts) = tagged(t)
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   364
        fs(tag)(ts)
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   365
      case ts => throw new XML_Body(ts)
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   366
    }
e0219ef7f84c tuned XML modules;
wenzelm
parents: 43747
diff changeset
   367
  }
27931
b533a9de87a7 Minimalistic XML tree values.
wenzelm
parents:
diff changeset
   368
}