author | wenzelm |
Fri, 04 Dec 2009 14:21:07 +0100 | |
changeset 33953 | 5e865ed88313 |
parent 29204 | e002f7b63e3c |
child 33999 | d3b200894e21 |
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 |
||
27947 | 9 |
import org.w3c.dom.{Node, Document} |
10 |
import javax.xml.parsers.DocumentBuilderFactory |
|
11 |
||
12 |
||
29203 | 13 |
object XML |
14 |
{ |
|
27947 | 15 |
/* datatype representation */ |
16 |
||
27931 | 17 |
type Attributes = List[(String, String)] |
18 |
||
29204 | 19 |
abstract class Tree { |
20 |
override def toString = { |
|
21 |
val s = new StringBuilder |
|
22 |
append_tree(this, s) |
|
23 |
s.toString |
|
24 |
} |
|
29203 | 25 |
} |
29204 | 26 |
case class Elem(name: String, attributes: Attributes, body: List[Tree]) extends Tree |
27 |
case class Text(content: String) extends Tree |
|
29203 | 28 |
|
29 |
||
30 |
/* string representation */ |
|
31 |
||
32 |
private def append_text(text: String, s: StringBuilder) { |
|
33 |
for (c <- text.elements) c match { |
|
34 |
case '<' => s.append("<") |
|
35 |
case '>' => s.append(">") |
|
36 |
case '&' => s.append("&") |
|
37 |
case '"' => s.append(""") |
|
38 |
case '\'' => s.append("'") |
|
29204 | 39 |
case _ => s.append(c) |
29203 | 40 |
} |
41 |
} |
|
42 |
||
43 |
private def append_elem(name: String, atts: Attributes, s: StringBuilder) { |
|
44 |
s.append(name) |
|
45 |
for ((a, x) <- atts) { |
|
46 |
s.append(" "); s.append(a); s.append("=\""); append_text(x, s); s.append("\"") |
|
47 |
} |
|
48 |
} |
|
49 |
||
29204 | 50 |
private def append_tree(tree: Tree, s: StringBuilder) { |
29203 | 51 |
tree match { |
52 |
case Elem(name, atts, Nil) => |
|
53 |
s.append("<"); append_elem(name, atts, s); s.append("/>") |
|
54 |
case Elem(name, atts, ts) => |
|
55 |
s.append("<"); append_elem(name, atts, s); s.append(">") |
|
56 |
for (t <- ts) append_tree(t, s) |
|
57 |
s.append("</"); s.append(name); s.append(">") |
|
58 |
case Text(text) => append_text(text, s) |
|
59 |
} |
|
60 |
} |
|
27941 | 61 |
|
62 |
||
27942 | 63 |
/* iterate over content */ |
27941 | 64 |
|
65 |
private type State = Option[(String, List[Tree])] |
|
66 |
||
67 |
private def get_next(tree: Tree): State = tree match { |
|
68 |
case Elem(_, _, body) => get_nexts(body) |
|
69 |
case Text(content) => Some(content, Nil) |
|
70 |
} |
|
71 |
private def get_nexts(trees: List[Tree]): State = trees match { |
|
72 |
case Nil => None |
|
73 |
case t :: ts => get_next(t) match { |
|
74 |
case None => get_nexts(ts) |
|
28007 | 75 |
case Some((s, r)) => Some((s, r ++ ts)) |
27941 | 76 |
} |
77 |
} |
|
78 |
||
79 |
def content(tree: Tree) = new Iterator[String] { |
|
80 |
private var state = get_next(tree) |
|
81 |
def hasNext() = state.isDefined |
|
82 |
def next() = state match { |
|
83 |
case Some((s, rest)) => { state = get_nexts(rest); s } |
|
84 |
case None => throw new NoSuchElementException("next on empty iterator") |
|
85 |
} |
|
86 |
} |
|
87 |
||
27947 | 88 |
|
33953 | 89 |
/* document object model (W3C DOM) */ |
27948
2638b611d3ce
renamed DOM to document, add xml version and optional stylesheets;
wenzelm
parents:
27947
diff
changeset
|
90 |
|
33953 | 91 |
def document_node(doc: Document, tree: Tree): Node = |
92 |
{ |
|
27952 | 93 |
def DOM(tr: Tree): Node = tr match { |
27947 | 94 |
case Elem(name, atts, ts) => { |
95 |
val node = doc.createElement(name) |
|
96 |
for ((name, value) <- atts) node.setAttribute(name, value) |
|
27952 | 97 |
for (t <- ts) node.appendChild(DOM(t)) |
27947 | 98 |
node |
99 |
} |
|
100 |
case Text(txt) => doc.createTextNode(txt) |
|
101 |
} |
|
33953 | 102 |
DOM(tree) |
103 |
} |
|
104 |
||
105 |
def document(tree: Tree, styles: String*): Document = |
|
106 |
{ |
|
107 |
val doc = DocumentBuilderFactory.newInstance.newDocumentBuilder.newDocument |
|
108 |
doc.appendChild(doc.createProcessingInstruction("xml", "version=\"1.0\"")) |
|
109 |
||
110 |
for (style <- styles) { |
|
111 |
doc.appendChild(doc.createProcessingInstruction("xml-stylesheet", |
|
112 |
"href=\"" + style + "\" type=\"text/css\"")) |
|
113 |
} |
|
27947 | 114 |
val root_elem = tree match { |
33953 | 115 |
case Elem(_, _, _) => document_node(doc, tree) |
116 |
case Text(_) => document_node(doc, (Elem(Markup.ROOT, Nil, List(tree)))) |
|
27947 | 117 |
} |
118 |
doc.appendChild(root_elem) |
|
119 |
doc |
|
120 |
} |
|
27931 | 121 |
} |