author | wenzelm |
Sun, 04 Sep 2011 14:29:15 +0200 | |
changeset 44697 | b99dfee76538 |
parent 43781 | d43e5f79bdc2 |
permissions | -rw-r--r-- |
27931 | 1 |
/* Title: Pure/General/xml.scala |
2 |
Author: Makarius |
|
3 |
||
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
4 |
Untyped XML trees. |
27931 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
43520
cec9b95fa35d
explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents:
38869
diff
changeset
|
9 |
import java.lang.System |
34108 | 10 |
import java.util.WeakHashMap |
11 |
import java.lang.ref.WeakReference |
|
12 |
import javax.xml.parsers.DocumentBuilderFactory |
|
13 |
||
38446
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
14 |
import scala.actors.Actor._ |
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
15 |
import scala.collection.mutable |
38446
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
16 |
|
27947 | 17 |
|
29203 | 18 |
object XML |
19 |
{ |
|
43767 | 20 |
/** XML trees **/ |
21 |
||
27947 | 22 |
/* datatype representation */ |
23 |
||
43780 | 24 |
type Attributes = Properties.T |
27931 | 25 |
|
38268
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
26 |
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
|
27 |
case class Elem(markup: Markup, body: List[Tree]) extends Tree |
29204 | 28 |
case class Text(content: String) extends Tree |
29203 | 29 |
|
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
36817
diff
changeset
|
30 |
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
|
31 |
def elem(name: String) = Elem(Markup(name, Nil), Nil) |
33999 | 32 |
|
38267
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
38263
diff
changeset
|
33 |
type Body = List[Tree] |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
38263
diff
changeset
|
34 |
|
29203 | 35 |
|
36 |
/* string representation */ |
|
37 |
||
38268
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
38 |
def string_of_body(body: Body): String = |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
39 |
{ |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
40 |
val s = new StringBuilder |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
41 |
|
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
42 |
def text(txt: String) { |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
43 |
if (txt == null) s ++= txt |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
44 |
else { |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
45 |
for (c <- txt.iterator) c match { |
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 ++= ">" |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
48 |
case '&' => s ++= "&" |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
49 |
case '"' => s ++= """ |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
50 |
case '\'' => s ++= "'" |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
51 |
case _ => s += c |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
52 |
} |
34005 | 53 |
} |
29203 | 54 |
} |
38268
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
55 |
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
|
56 |
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
|
57 |
def tree(t: Tree): Unit = |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
58 |
t match { |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
59 |
case Elem(markup, Nil) => |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
60 |
s ++= "<"; elem(markup); s ++= "/>" |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
61 |
case Elem(markup, ts) => |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
62 |
s ++= "<"; elem(markup); s ++= ">" |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
63 |
ts.foreach(tree) |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
64 |
s ++= "</"; s ++= markup.name; s ++= ">" |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
65 |
case Text(txt) => text(txt) |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
66 |
} |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
67 |
body.foreach(tree) |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
68 |
s.toString |
29203 | 69 |
} |
70 |
||
38268
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
71 |
def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree)) |
27941 | 72 |
|
73 |
||
38484
9c1fde4e2487
tuned XML.content: Stream based iteration is supposed to be declarative *and* efficient;
wenzelm
parents:
38446
diff
changeset
|
74 |
/* text content */ |
27941 | 75 |
|
38484
9c1fde4e2487
tuned XML.content: Stream based iteration is supposed to be declarative *and* efficient;
wenzelm
parents:
38446
diff
changeset
|
76 |
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
|
77 |
tree match { |
43747 | 78 |
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
|
79 |
case Text(content) => Stream(content) |
27941 | 80 |
} |
43747 | 81 |
def content_stream(body: Body): Stream[String] = |
82 |
body.toStream.flatten(content_stream(_)) |
|
27941 | 83 |
|
38484
9c1fde4e2487
tuned XML.content: Stream based iteration is supposed to be declarative *and* efficient;
wenzelm
parents:
38446
diff
changeset
|
84 |
def content(tree: Tree): Iterator[String] = content_stream(tree).iterator |
43747 | 85 |
def content(body: Body): Iterator[String] = content_stream(body).iterator |
27941 | 86 |
|
27947 | 87 |
|
38446
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
88 |
/* pipe-lined cache for partial sharing */ |
34108 | 89 |
|
43745 | 90 |
class Cache(initial_size: Int = 131071, max_string: Int = 100) |
34108 | 91 |
{ |
38446
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
92 |
private val cache_actor = actor |
34108 | 93 |
{ |
38446
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
94 |
val table = new WeakHashMap[Any, WeakReference[Any]](initial_size) |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
95 |
|
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
96 |
def lookup[A](x: A): Option[A] = |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
97 |
{ |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
98 |
val ref = table.get(x) |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
99 |
if (ref == null) None |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
100 |
else { |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
101 |
val y = ref.asInstanceOf[WeakReference[A]].get |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
102 |
if (y == null) None |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
103 |
else Some(y) |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
104 |
} |
34108 | 105 |
} |
38446
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
106 |
def store[A](x: A): A = |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
107 |
{ |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
108 |
table.put(x, new WeakReference[Any](x)) |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
109 |
x |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
110 |
} |
34108 | 111 |
|
38869 | 112 |
def trim_bytes(s: String): String = new String(s.toCharArray) |
113 |
||
38446
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
114 |
def cache_string(x: String): String = |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
115 |
lookup(x) match { |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
116 |
case Some(y) => y |
43745 | 117 |
case None => |
118 |
val z = trim_bytes(x) |
|
119 |
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
|
120 |
} |
43780 | 121 |
def cache_props(x: Properties.T): Properties.T = |
38446
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
122 |
if (x.isEmpty) x |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
123 |
else |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
124 |
lookup(x) match { |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
125 |
case Some(y) => y |
38869 | 126 |
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
|
127 |
} |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
128 |
def cache_markup(x: Markup): Markup = |
34133 | 129 |
lookup(x) match { |
130 |
case Some(y) => y |
|
38446
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
131 |
case None => |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
132 |
x match { |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
133 |
case Markup(name, props) => |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
134 |
store(Markup(cache_string(name), cache_props(props))) |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
135 |
} |
34133 | 136 |
} |
38446
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
137 |
def cache_tree(x: XML.Tree): XML.Tree = |
34133 | 138 |
lookup(x) match { |
139 |
case Some(y) => y |
|
38446
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
140 |
case None => |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
141 |
x match { |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
142 |
case XML.Elem(markup, body) => |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
143 |
store(XML.Elem(cache_markup(markup), cache_body(body))) |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
144 |
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
|
145 |
} |
34133 | 146 |
} |
38446
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
147 |
def cache_body(x: XML.Body): XML.Body = |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
148 |
if (x.isEmpty) x |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
149 |
else |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
150 |
lookup(x) match { |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
151 |
case Some(y) => y |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
152 |
case None => x.map(cache_tree(_)) |
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 |
|
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
155 |
// main loop |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
156 |
loop { |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
157 |
react { |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
158 |
case Cache_String(x, f) => f(cache_string(x)) |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
159 |
case Cache_Markup(x, f) => f(cache_markup(x)) |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
160 |
case Cache_Tree(x, f) => f(cache_tree(x)) |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
161 |
case Cache_Body(x, f) => f(cache_body(x)) |
44697
b99dfee76538
pass raw messages through xml_cache actor, which is important to retain ordering of results (e.g. read_command reports before assign, cf. 383c9d758a56);
wenzelm
parents:
43781
diff
changeset
|
162 |
case Cache_Ignore(x, f) => f(x) |
38446
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
163 |
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
|
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 |
} |
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 |
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
|
169 |
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
|
170 |
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
|
171 |
private case class Cache_Body(x: XML.Body, f: XML.Body => Unit) |
44697
b99dfee76538
pass raw messages through xml_cache actor, which is important to retain ordering of results (e.g. read_command reports before assign, cf. 383c9d758a56);
wenzelm
parents:
43781
diff
changeset
|
172 |
private case class Cache_Ignore[A](x: A, f: A => Unit) |
38446
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
173 |
|
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
174 |
// main methods |
9d59dab38fef
XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents:
38268
diff
changeset
|
175 |
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
|
176 |
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
|
177 |
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
|
178 |
def cache_body(x: XML.Body)(f: XML.Body => Unit) { cache_actor ! Cache_Body(x, f) } |
44697
b99dfee76538
pass raw messages through xml_cache actor, which is important to retain ordering of results (e.g. read_command reports before assign, cf. 383c9d758a56);
wenzelm
parents:
43781
diff
changeset
|
179 |
def cache_ignore[A](x: A)(f: A => Unit) { cache_actor ! Cache_Ignore(x, f) } |
34108 | 180 |
} |
181 |
||
182 |
||
43767 | 183 |
|
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 |
} |
|
43767 | 210 |
|
211 |
||
212 |
||
213 |
/** XML as data representation language **/ |
|
214 |
||
215 |
class XML_Atom(s: String) extends Exception(s) |
|
216 |
class XML_Body(body: XML.Body) extends Exception |
|
217 |
||
218 |
object Encode |
|
219 |
{ |
|
220 |
type T[A] = A => XML.Body |
|
221 |
||
222 |
||
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
223 |
/* atomic values */ |
43767 | 224 |
|
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
225 |
def long_atom(i: Long): String = i.toString |
43767 | 226 |
|
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
227 |
def int_atom(i: Int): String = i.toString |
43767 | 228 |
|
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
229 |
def bool_atom(b: Boolean): String = if (b) "1" else "0" |
43767 | 230 |
|
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
231 |
def unit_atom(u: Unit) = "" |
43767 | 232 |
|
233 |
||
234 |
/* structural nodes */ |
|
235 |
||
236 |
private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts) |
|
237 |
||
43781 | 238 |
private def vector(xs: List[String]): XML.Attributes = |
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
239 |
xs.zipWithIndex.map(p => (int_atom(p._2), p._1)) |
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
240 |
|
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
241 |
private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree = |
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
242 |
XML.Elem(Markup(int_atom(tag), vector(data._1)), data._2) |
43767 | 243 |
|
244 |
||
245 |
/* representation of standard types */ |
|
246 |
||
43780 | 247 |
val properties: T[Properties.T] = |
43767 | 248 |
(props => List(XML.Elem(Markup(":", props), Nil))) |
249 |
||
250 |
val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s))) |
|
251 |
||
252 |
val long: T[Long] = (x => string(long_atom(x))) |
|
253 |
||
254 |
val int: T[Int] = (x => string(int_atom(x))) |
|
255 |
||
256 |
val bool: T[Boolean] = (x => string(bool_atom(x))) |
|
257 |
||
258 |
val unit: T[Unit] = (x => string(unit_atom(x))) |
|
259 |
||
260 |
def pair[A, B](f: T[A], g: T[B]): T[(A, B)] = |
|
261 |
(x => List(node(f(x._1)), node(g(x._2)))) |
|
262 |
||
263 |
def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] = |
|
264 |
(x => List(node(f(x._1)), node(g(x._2)), node(h(x._3)))) |
|
265 |
||
266 |
def list[A](f: T[A]): T[List[A]] = |
|
267 |
(xs => xs.map((x: A) => node(f(x)))) |
|
268 |
||
269 |
def option[A](f: T[A]): T[Option[A]] = |
|
270 |
{ |
|
271 |
case None => Nil |
|
272 |
case Some(x) => List(node(f(x))) |
|
273 |
} |
|
274 |
||
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
275 |
def variant[A](fs: List[PartialFunction[A, (List[String], XML.Body)]]): T[A] = |
43767 | 276 |
{ |
277 |
case x => |
|
278 |
val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get |
|
279 |
List(tagged(tag, f(x))) |
|
280 |
} |
|
281 |
} |
|
282 |
||
283 |
object Decode |
|
284 |
{ |
|
285 |
type T[A] = XML.Body => A |
|
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
286 |
type V[A] = (List[String], XML.Body) => A |
43767 | 287 |
|
288 |
||
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
289 |
/* atomic values */ |
43767 | 290 |
|
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
291 |
def long_atom(s: String): Long = |
43767 | 292 |
try { java.lang.Long.parseLong(s) } |
293 |
catch { case e: NumberFormatException => throw new XML_Atom(s) } |
|
294 |
||
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
295 |
def int_atom(s: String): Int = |
43767 | 296 |
try { Integer.parseInt(s) } |
297 |
catch { case e: NumberFormatException => throw new XML_Atom(s) } |
|
298 |
||
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
299 |
def bool_atom(s: String): Boolean = |
43767 | 300 |
if (s == "1") true |
301 |
else if (s == "0") false |
|
302 |
else throw new XML_Atom(s) |
|
303 |
||
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
304 |
def unit_atom(s: String): Unit = |
43767 | 305 |
if (s == "") () else throw new XML_Atom(s) |
306 |
||
307 |
||
308 |
/* structural nodes */ |
|
309 |
||
310 |
private def node(t: XML.Tree): XML.Body = |
|
311 |
t match { |
|
312 |
case XML.Elem(Markup(":", Nil), ts) => ts |
|
313 |
case _ => throw new XML_Body(List(t)) |
|
314 |
} |
|
315 |
||
43781 | 316 |
private def vector(atts: XML.Attributes): List[String] = |
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
317 |
{ |
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
318 |
val xs = new mutable.ListBuffer[String] |
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
319 |
var i = 0 |
43781 | 320 |
for ((a, x) <- atts) { |
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
321 |
if (int_atom(a) == i) { xs += x; i = i + 1 } |
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
322 |
else throw new XML_Atom(a) |
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
323 |
} |
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
324 |
xs.toList |
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
325 |
} |
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
326 |
|
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
327 |
private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) = |
43767 | 328 |
t match { |
43781 | 329 |
case XML.Elem(Markup(name, atts), ts) => (int_atom(name), (vector(atts), ts)) |
43767 | 330 |
case _ => throw new XML_Body(List(t)) |
331 |
} |
|
332 |
||
333 |
||
334 |
/* representation of standard types */ |
|
335 |
||
43780 | 336 |
val properties: T[Properties.T] = |
43767 | 337 |
{ |
338 |
case List(XML.Elem(Markup(":", props), Nil)) => props |
|
339 |
case ts => throw new XML_Body(ts) |
|
340 |
} |
|
341 |
||
342 |
val string: T[String] = |
|
343 |
{ |
|
344 |
case Nil => "" |
|
345 |
case List(XML.Text(s)) => s |
|
346 |
case ts => throw new XML_Body(ts) |
|
347 |
} |
|
348 |
||
349 |
val long: T[Long] = (x => long_atom(string(x))) |
|
350 |
||
351 |
val int: T[Int] = (x => int_atom(string(x))) |
|
352 |
||
353 |
val bool: T[Boolean] = (x => bool_atom(string(x))) |
|
354 |
||
355 |
val unit: T[Unit] = (x => unit_atom(string(x))) |
|
356 |
||
357 |
def pair[A, B](f: T[A], g: T[B]): T[(A, B)] = |
|
358 |
{ |
|
359 |
case List(t1, t2) => (f(node(t1)), g(node(t2))) |
|
360 |
case ts => throw new XML_Body(ts) |
|
361 |
} |
|
362 |
||
363 |
def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] = |
|
364 |
{ |
|
365 |
case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3))) |
|
366 |
case ts => throw new XML_Body(ts) |
|
367 |
} |
|
368 |
||
369 |
def list[A](f: T[A]): T[List[A]] = |
|
370 |
(ts => ts.map(t => f(node(t)))) |
|
371 |
||
372 |
def option[A](f: T[A]): T[Option[A]] = |
|
373 |
{ |
|
374 |
case Nil => None |
|
375 |
case List(t) => Some(f(node(t))) |
|
376 |
case ts => throw new XML_Body(ts) |
|
377 |
} |
|
378 |
||
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
379 |
def variant[A](fs: List[V[A]]): T[A] = |
43767 | 380 |
{ |
381 |
case List(t) => |
|
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
382 |
val (tag, (xs, ts)) = tagged(t) |
43768 | 383 |
val f = |
384 |
try { fs(tag) } |
|
385 |
catch { case _: IndexOutOfBoundsException => throw new XML_Body(List(t)) } |
|
43778
ce9189450447
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
wenzelm
parents:
43768
diff
changeset
|
386 |
f(xs, ts) |
43767 | 387 |
case ts => throw new XML_Body(ts) |
388 |
} |
|
389 |
} |
|
27931 | 390 |
} |