author | wenzelm |
Fri, 19 Dec 2008 20:37:29 +0100 | |
changeset 29140 | e7ac5bb20aed |
parent 28007 | 2d0c93291293 |
child 29203 | 0c4effb73518 |
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 |
||
27931 | 13 |
object XML { |
27947 | 14 |
/* datatype representation */ |
15 |
||
27931 | 16 |
type Attributes = List[(String, String)] |
17 |
||
18 |
abstract class Tree |
|
19 |
case class Elem(name: String, attributes: Attributes, body: List[Tree]) extends Tree |
|
20 |
case class Text(content: String) extends Tree |
|
27941 | 21 |
|
22 |
||
27942 | 23 |
/* iterate over content */ |
27941 | 24 |
|
25 |
private type State = Option[(String, List[Tree])] |
|
26 |
||
27 |
private def get_next(tree: Tree): State = tree match { |
|
28 |
case Elem(_, _, body) => get_nexts(body) |
|
29 |
case Text(content) => Some(content, Nil) |
|
30 |
} |
|
31 |
private def get_nexts(trees: List[Tree]): State = trees match { |
|
32 |
case Nil => None |
|
33 |
case t :: ts => get_next(t) match { |
|
34 |
case None => get_nexts(ts) |
|
28007 | 35 |
case Some((s, r)) => Some((s, r ++ ts)) |
27941 | 36 |
} |
37 |
} |
|
38 |
||
39 |
def content(tree: Tree) = new Iterator[String] { |
|
40 |
private var state = get_next(tree) |
|
41 |
def hasNext() = state.isDefined |
|
42 |
def next() = state match { |
|
43 |
case Some((s, rest)) => { state = get_nexts(rest); s } |
|
44 |
case None => throw new NoSuchElementException("next on empty iterator") |
|
45 |
} |
|
46 |
} |
|
47 |
||
27947 | 48 |
|
49 |
/* document object model (DOM) */ |
|
50 |
||
27948
2638b611d3ce
renamed DOM to document, add xml version and optional stylesheets;
wenzelm
parents:
27947
diff
changeset
|
51 |
def document(tree: Tree, styles: String*) = { |
27947 | 52 |
val doc = DocumentBuilderFactory.newInstance.newDocumentBuilder.newDocument |
27948
2638b611d3ce
renamed DOM to document, add xml version and optional stylesheets;
wenzelm
parents:
27947
diff
changeset
|
53 |
doc.appendChild(doc.createProcessingInstruction("xml", "version=\"1.0\"")) |
2638b611d3ce
renamed DOM to document, add xml version and optional stylesheets;
wenzelm
parents:
27947
diff
changeset
|
54 |
|
2638b611d3ce
renamed DOM to document, add xml version and optional stylesheets;
wenzelm
parents:
27947
diff
changeset
|
55 |
for (style <- styles) { |
2638b611d3ce
renamed DOM to document, add xml version and optional stylesheets;
wenzelm
parents:
27947
diff
changeset
|
56 |
doc.appendChild(doc.createProcessingInstruction("xml-stylesheet", |
2638b611d3ce
renamed DOM to document, add xml version and optional stylesheets;
wenzelm
parents:
27947
diff
changeset
|
57 |
"href=\"" + style + "\" type=\"text/css\"")) |
2638b611d3ce
renamed DOM to document, add xml version and optional stylesheets;
wenzelm
parents:
27947
diff
changeset
|
58 |
} |
2638b611d3ce
renamed DOM to document, add xml version and optional stylesheets;
wenzelm
parents:
27947
diff
changeset
|
59 |
|
2638b611d3ce
renamed DOM to document, add xml version and optional stylesheets;
wenzelm
parents:
27947
diff
changeset
|
60 |
// main body |
27952 | 61 |
def DOM(tr: Tree): Node = tr match { |
27947 | 62 |
case Elem(name, atts, ts) => { |
63 |
val node = doc.createElement(name) |
|
64 |
for ((name, value) <- atts) node.setAttribute(name, value) |
|
27952 | 65 |
for (t <- ts) node.appendChild(DOM(t)) |
27947 | 66 |
node |
67 |
} |
|
68 |
case Text(txt) => doc.createTextNode(txt) |
|
69 |
} |
|
70 |
val root_elem = tree match { |
|
27952 | 71 |
case Elem(_, _, _) => DOM(tree) |
27959 | 72 |
case Text(_) => DOM(Elem(Markup.ROOT, Nil, List(tree))) |
27947 | 73 |
} |
74 |
doc.appendChild(root_elem) |
|
75 |
doc |
|
76 |
} |
|
27931 | 77 |
} |