author | wenzelm |
Sun, 30 May 2010 14:14:30 +0200 | |
changeset 37192 | 8cdddd689ea9 |
parent 36817 | ed97e877ff2d |
child 38230 | ed147003de4b |
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 |
||
27947 | 13 |
|
29203 | 14 |
object XML |
15 |
{ |
|
27947 | 16 |
/* datatype representation */ |
17 |
||
27931 | 18 |
type Attributes = List[(String, String)] |
19 |
||
34046 | 20 |
sealed abstract class Tree { |
29204 | 21 |
override def toString = { |
22 |
val s = new StringBuilder |
|
23 |
append_tree(this, s) |
|
24 |
s.toString |
|
25 |
} |
|
29203 | 26 |
} |
29204 | 27 |
case class Elem(name: String, attributes: Attributes, body: List[Tree]) extends Tree |
28 |
case class Text(content: String) extends Tree |
|
29203 | 29 |
|
33999 | 30 |
def elem(name: String, body: List[Tree]) = Elem(name, Nil, body) |
31 |
def elem(name: String) = Elem(name, Nil, Nil) |
|
32 |
||
29203 | 33 |
|
34 |
/* string representation */ |
|
35 |
||
36 |
private def append_text(text: String, s: StringBuilder) { |
|
36016
4f5c7a19ebe0
recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;
wenzelm
parents:
36011
diff
changeset
|
37 |
if (text == null) s ++= text |
34005 | 38 |
else { |
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34871
diff
changeset
|
39 |
for (c <- text.iterator) c match { |
36016
4f5c7a19ebe0
recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;
wenzelm
parents:
36011
diff
changeset
|
40 |
case '<' => s ++= "<" |
4f5c7a19ebe0
recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;
wenzelm
parents:
36011
diff
changeset
|
41 |
case '>' => s ++= ">" |
4f5c7a19ebe0
recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;
wenzelm
parents:
36011
diff
changeset
|
42 |
case '&' => s ++= "&" |
4f5c7a19ebe0
recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;
wenzelm
parents:
36011
diff
changeset
|
43 |
case '"' => s ++= """ |
4f5c7a19ebe0
recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;
wenzelm
parents:
36011
diff
changeset
|
44 |
case '\'' => s ++= "'" |
4f5c7a19ebe0
recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;
wenzelm
parents:
36011
diff
changeset
|
45 |
case _ => s += c |
34005 | 46 |
} |
29203 | 47 |
} |
48 |
} |
|
49 |
||
50 |
private def append_elem(name: String, atts: Attributes, s: StringBuilder) { |
|
36016
4f5c7a19ebe0
recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;
wenzelm
parents:
36011
diff
changeset
|
51 |
s ++= name |
29203 | 52 |
for ((a, x) <- atts) { |
36016
4f5c7a19ebe0
recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;
wenzelm
parents:
36011
diff
changeset
|
53 |
s ++= " "; s ++= a; s ++= "=\""; append_text(x, s); s ++= "\"" |
29203 | 54 |
} |
55 |
} |
|
56 |
||
29204 | 57 |
private def append_tree(tree: Tree, s: StringBuilder) { |
29203 | 58 |
tree match { |
59 |
case Elem(name, atts, Nil) => |
|
36016
4f5c7a19ebe0
recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;
wenzelm
parents:
36011
diff
changeset
|
60 |
s ++= "<"; append_elem(name, atts, s); s ++= "/>" |
29203 | 61 |
case Elem(name, atts, ts) => |
36016
4f5c7a19ebe0
recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;
wenzelm
parents:
36011
diff
changeset
|
62 |
s ++= "<"; append_elem(name, atts, s); s ++= ">" |
29203 | 63 |
for (t <- ts) append_tree(t, s) |
36016
4f5c7a19ebe0
recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;
wenzelm
parents:
36011
diff
changeset
|
64 |
s ++= "</"; s ++= name; s ++= ">" |
29203 | 65 |
case Text(text) => append_text(text, s) |
66 |
} |
|
67 |
} |
|
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 { |
|
75 |
case Elem(_, _, body) => get_nexts(body) |
|
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 |
|
34108 | 96 |
/* cache for partial sharing -- NOT THREAD SAFE */ |
97 |
||
98 |
class Cache(initial_size: Int) |
|
99 |
{ |
|
100 |
private val table = new WeakHashMap[Any, WeakReference[Any]](initial_size) |
|
101 |
||
102 |
private def lookup[A](x: A): Option[A] = |
|
103 |
{ |
|
104 |
val ref = table.get(x) |
|
105 |
if (ref == null) None |
|
106 |
else { |
|
107 |
val y = ref.asInstanceOf[WeakReference[A]].get |
|
108 |
if (y == null) None |
|
109 |
else Some(y) |
|
110 |
} |
|
111 |
} |
|
112 |
private def store[A](x: A): A = |
|
113 |
{ |
|
114 |
table.put(x, new WeakReference[Any](x)) |
|
115 |
x |
|
116 |
} |
|
117 |
||
118 |
def cache_string(x: String): String = |
|
119 |
lookup(x) match { |
|
120 |
case Some(y) => y |
|
121 |
case None => store(x) |
|
122 |
} |
|
123 |
def cache_props(x: List[(String, String)]): List[(String, String)] = |
|
34133 | 124 |
if (x.isEmpty) x |
125 |
else |
|
126 |
lookup(x) match { |
|
127 |
case Some(y) => y |
|
128 |
case None => store(x.map(p => (cache_string(p._1), cache_string(p._2)))) |
|
129 |
} |
|
34117 | 130 |
def cache_tree(x: XML.Tree): XML.Tree = |
34108 | 131 |
lookup(x) match { |
132 |
case Some(y) => y |
|
133 |
case None => |
|
134 |
x match { |
|
135 |
case XML.Elem(name, props, body) => |
|
34117 | 136 |
store(XML.Elem(cache_string(name), cache_props(props), cache_trees(body))) |
34108 | 137 |
case XML.Text(text) => XML.Text(cache_string(text)) |
138 |
} |
|
139 |
} |
|
34117 | 140 |
def cache_trees(x: List[XML.Tree]): List[XML.Tree] = |
34133 | 141 |
if (x.isEmpty) x |
142 |
else |
|
143 |
lookup(x) match { |
|
144 |
case Some(y) => y |
|
145 |
case None => x.map(cache_tree(_)) |
|
146 |
} |
|
34108 | 147 |
} |
148 |
||
149 |
||
33953 | 150 |
/* document object model (W3C DOM) */ |
27948
2638b611d3ce
renamed DOM to document, add xml version and optional stylesheets;
wenzelm
parents:
27947
diff
changeset
|
151 |
|
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
|
152 |
def get_data(node: org.w3c.dom.Node): Option[XML.Tree] = |
34047 | 153 |
node.getUserData(Markup.DATA) match { |
154 |
case tree: XML.Tree => Some(tree) |
|
155 |
case _ => None |
|
156 |
} |
|
157 |
||
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
|
158 |
def document_node(doc: org.w3c.dom.Document, tree: Tree): org.w3c.dom.Node = |
33953 | 159 |
{ |
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
|
160 |
def DOM(tr: Tree): org.w3c.dom.Node = tr match { |
34046 | 161 |
case Elem(Markup.DATA, Nil, List(data, t)) => |
162 |
val node = DOM(t) |
|
163 |
node.setUserData(Markup.DATA, data, null) |
|
164 |
node |
|
165 |
case Elem(name, atts, ts) => |
|
166 |
if (name == Markup.DATA) |
|
167 |
error("Malformed data element: " + tr.toString) |
|
27947 | 168 |
val node = doc.createElement(name) |
169 |
for ((name, value) <- atts) node.setAttribute(name, value) |
|
27952 | 170 |
for (t <- ts) node.appendChild(DOM(t)) |
27947 | 171 |
node |
172 |
case Text(txt) => doc.createTextNode(txt) |
|
173 |
} |
|
33953 | 174 |
DOM(tree) |
175 |
} |
|
27931 | 176 |
} |