author | wenzelm |
Mon, 16 Aug 2010 18:20:36 +0200 | |
changeset 38446 | 9d59dab38fef |
parent 38268 | beb86b805590 |
child 38484 | 9c1fde4e2487 |
permissions | -rw-r--r-- |
27931 | 1 |
/* Title: Pure/General/xml.scala |
2 |
Author: Makarius |
|
3 |
||
27947 | 4 |
Simple XML tree values. |
27931 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
34108 | 9 |
import java.util.WeakHashMap |
10 |
import java.lang.ref.WeakReference |
|
11 |
import javax.xml.parsers.DocumentBuilderFactory |
|
12 |
||
38446
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
13 |
import scala.actors.Actor._ |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
14 |
|
27947 | 15 |
|
29203 | 16 |
object XML |
17 |
{ |
|
27947 | 18 |
/* datatype representation */ |
19 |
||
27931 | 20 |
type Attributes = List[(String, String)] |
21 |
||
38268
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
22 |
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
|
23 |
case class Elem(markup: Markup, body: List[Tree]) extends Tree |
29204 | 24 |
case class Text(content: String) extends Tree |
29203 | 25 |
|
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
36817
diff
changeset
|
26 |
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
|
27 |
def elem(name: String) = Elem(Markup(name, Nil), Nil) |
33999 | 28 |
|
38267
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
38263
diff
changeset
|
29 |
type Body = List[Tree] |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
38263
diff
changeset
|
30 |
|
29203 | 31 |
|
32 |
/* string representation */ |
|
33 |
||
38268
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
34 |
def string_of_body(body: Body): String = |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
35 |
{ |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
36 |
val s = new StringBuilder |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
37 |
|
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
38 |
def text(txt: String) { |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
39 |
if (txt == null) s ++= txt |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
40 |
else { |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
41 |
for (c <- txt.iterator) c match { |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
42 |
case '<' => s ++= "<" |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
43 |
case '>' => s ++= ">" |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
44 |
case '&' => s ++= "&" |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
45 |
case '"' => s ++= """ |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
46 |
case '\'' => s ++= "'" |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
47 |
case _ => s += c |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
48 |
} |
34005 | 49 |
} |
29203 | 50 |
} |
38268
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
51 |
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
|
52 |
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
|
53 |
def tree(t: Tree): Unit = |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
54 |
t match { |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
55 |
case Elem(markup, Nil) => |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
56 |
s ++= "<"; elem(markup); s ++= "/>" |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
57 |
case Elem(markup, ts) => |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
58 |
s ++= "<"; elem(markup); s ++= ">" |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
59 |
ts.foreach(tree) |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
60 |
s ++= "</"; s ++= markup.name; s ++= ">" |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
61 |
case Text(txt) => text(txt) |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
62 |
} |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
63 |
body.foreach(tree) |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
64 |
s.toString |
29203 | 65 |
} |
66 |
||
38268
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
67 |
def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree)) |
27941 | 68 |
|
69 |
||
27942 | 70 |
/* iterate over content */ |
27941 | 71 |
|
72 |
private type State = Option[(String, List[Tree])] |
|
73 |
||
74 |
private def get_next(tree: Tree): State = tree match { |
|
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
36817
diff
changeset
|
75 |
case Elem(_, body) => get_nexts(body) |
27941 | 76 |
case Text(content) => Some(content, Nil) |
77 |
} |
|
78 |
private def get_nexts(trees: List[Tree]): State = trees match { |
|
79 |
case Nil => None |
|
80 |
case t :: ts => get_next(t) match { |
|
81 |
case None => get_nexts(ts) |
|
28007 | 82 |
case Some((s, r)) => Some((s, r ++ ts)) |
27941 | 83 |
} |
84 |
} |
|
85 |
||
86 |
def content(tree: Tree) = new Iterator[String] { |
|
87 |
private var state = get_next(tree) |
|
88 |
def hasNext() = state.isDefined |
|
89 |
def next() = state match { |
|
90 |
case Some((s, rest)) => { state = get_nexts(rest); s } |
|
91 |
case None => throw new NoSuchElementException("next on empty iterator") |
|
92 |
} |
|
93 |
} |
|
94 |
||
27947 | 95 |
|
38446
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
96 |
/* pipe-lined cache for partial sharing */ |
34108 | 97 |
|
98 |
class Cache(initial_size: Int) |
|
99 |
{ |
|
38446
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
100 |
private val cache_actor = actor |
34108 | 101 |
{ |
38446
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
102 |
val table = new WeakHashMap[Any, WeakReference[Any]](initial_size) |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
103 |
|
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
104 |
def lookup[A](x: A): Option[A] = |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
105 |
{ |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
106 |
val ref = table.get(x) |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
107 |
if (ref == null) None |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
108 |
else { |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
109 |
val y = ref.asInstanceOf[WeakReference[A]].get |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
110 |
if (y == null) None |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
111 |
else Some(y) |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
112 |
} |
34108 | 113 |
} |
38446
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
114 |
def store[A](x: A): A = |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
115 |
{ |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
116 |
table.put(x, new WeakReference[Any](x)) |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
117 |
x |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
118 |
} |
34108 | 119 |
|
38446
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
120 |
def cache_string(x: String): String = |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
121 |
lookup(x) match { |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
122 |
case Some(y) => y |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
123 |
case None => store(new String(x.toCharArray)) // trim string value |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
124 |
} |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
125 |
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
|
126 |
if (x.isEmpty) x |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
127 |
else |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
128 |
lookup(x) match { |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
129 |
case Some(y) => y |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
130 |
case None => store(x.map(p => (cache_string(p._1), cache_string(p._2)))) |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
131 |
} |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
132 |
def cache_markup(x: Markup): Markup = |
34133 | 133 |
lookup(x) match { |
134 |
case Some(y) => y |
|
38446
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
135 |
case None => |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
136 |
x match { |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
137 |
case Markup(name, props) => |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
138 |
store(Markup(cache_string(name), cache_props(props))) |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
139 |
} |
34133 | 140 |
} |
38446
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
141 |
def cache_tree(x: XML.Tree): XML.Tree = |
34133 | 142 |
lookup(x) match { |
143 |
case Some(y) => y |
|
38446
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
144 |
case None => |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
145 |
x match { |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
146 |
case XML.Elem(markup, body) => |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
147 |
store(XML.Elem(cache_markup(markup), cache_body(body))) |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
148 |
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
|
149 |
} |
34133 | 150 |
} |
38446
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
151 |
def cache_body(x: XML.Body): XML.Body = |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
152 |
if (x.isEmpty) x |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
153 |
else |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
154 |
lookup(x) match { |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
155 |
case Some(y) => y |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
156 |
case None => x.map(cache_tree(_)) |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
157 |
} |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
158 |
|
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
159 |
// main loop |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
160 |
loop { |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
161 |
react { |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
162 |
case Cache_String(x, f) => f(cache_string(x)) |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
163 |
case Cache_Markup(x, f) => f(cache_markup(x)) |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
164 |
case Cache_Tree(x, f) => f(cache_tree(x)) |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
165 |
case Cache_Body(x, f) => f(cache_body(x)) |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
166 |
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
|
167 |
} |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
168 |
} |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
169 |
} |
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 |
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
|
172 |
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
|
173 |
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
|
174 |
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
|
175 |
|
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
176 |
// main methods |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
177 |
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
|
178 |
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
|
179 |
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
|
180 |
def cache_body(x: XML.Body)(f: XML.Body => Unit) { cache_actor ! Cache_Body(x, f) } |
34108 | 181 |
} |
182 |
||
183 |
||
33953 | 184 |
/* document object model (W3C DOM) */ |
27948
2638b611d3ce
renamed DOM to document, add xml version and optional stylesheets;
wenzelm
parents:
27947
diff
changeset
|
185 |
|
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
|
186 |
def get_data(node: org.w3c.dom.Node): Option[XML.Tree] = |
38231 | 187 |
node.getUserData(Markup.Data.name) match { |
34047 | 188 |
case tree: XML.Tree => Some(tree) |
189 |
case _ => None |
|
190 |
} |
|
191 |
||
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
|
192 |
def document_node(doc: org.w3c.dom.Document, tree: Tree): org.w3c.dom.Node = |
33953 | 193 |
{ |
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
|
194 |
def DOM(tr: Tree): org.w3c.dom.Node = tr match { |
38231 | 195 |
case Elem(Markup.Data, List(data, t)) => |
34046 | 196 |
val node = DOM(t) |
38231 | 197 |
node.setUserData(Markup.Data.name, data, null) |
34046 | 198 |
node |
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
36817
diff
changeset
|
199 |
case Elem(Markup(name, atts), ts) => |
38231 | 200 |
if (name == Markup.Data.name) |
34046 | 201 |
error("Malformed data element: " + tr.toString) |
27947 | 202 |
val node = doc.createElement(name) |
203 |
for ((name, value) <- atts) node.setAttribute(name, value) |
|
27952 | 204 |
for (t <- ts) node.appendChild(DOM(t)) |
27947 | 205 |
node |
206 |
case Text(txt) => doc.createTextNode(txt) |
|
207 |
} |
|
33953 | 208 |
DOM(tree) |
209 |
} |
|
27931 | 210 |
} |