author | wenzelm |
Fri, 18 Dec 2009 12:28:50 +0100 | |
changeset 34119 | ae92efb48784 |
parent 34118 | ee9f87e11400 |
child 34191 | b6960fc09ef3 |
permissions | -rw-r--r-- |
27930 | 1 |
/* Title: Pure/General/yxml.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Efficient text representation of XML trees. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
32450 | 10 |
object YXML |
11 |
{ |
|
27943
f34ff5e7728f
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
wenzelm
parents:
27930
diff
changeset
|
12 |
/* chunk markers */ |
27930 | 13 |
|
14 |
private val X = '\5' |
|
15 |
private val Y = '\6' |
|
27960 | 16 |
private val X_string = X.toString |
27945
d2dc5a1903e8
tuned parse performance: avoid splitting terminal Y chunk;
wenzelm
parents:
27944
diff
changeset
|
17 |
private val Y_string = Y.toString |
27930 | 18 |
|
19 |
||
27943
f34ff5e7728f
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
wenzelm
parents:
27930
diff
changeset
|
20 |
/* iterate over chunks (resembles space_explode in ML) */ |
f34ff5e7728f
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
wenzelm
parents:
27930
diff
changeset
|
21 |
|
34099
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
22 |
private def chunks(sep: Char, source: CharSequence) = new Iterator[CharSequence] |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
23 |
{ |
27943
f34ff5e7728f
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
wenzelm
parents:
27930
diff
changeset
|
24 |
private val end = source.length |
f34ff5e7728f
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
wenzelm
parents:
27930
diff
changeset
|
25 |
private var state = if (end == 0) None else get_chunk(-1) |
32450 | 26 |
private def get_chunk(i: Int) = |
27 |
{ |
|
27943
f34ff5e7728f
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
wenzelm
parents:
27930
diff
changeset
|
28 |
if (i < end) { |
f34ff5e7728f
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
wenzelm
parents:
27930
diff
changeset
|
29 |
var j = i; do j += 1 while (j < end && source.charAt(j) != sep) |
f34ff5e7728f
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
wenzelm
parents:
27930
diff
changeset
|
30 |
Some((source.subSequence(i + 1, j), j)) |
f34ff5e7728f
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
wenzelm
parents:
27930
diff
changeset
|
31 |
} |
f34ff5e7728f
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
wenzelm
parents:
27930
diff
changeset
|
32 |
else None |
f34ff5e7728f
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
wenzelm
parents:
27930
diff
changeset
|
33 |
} |
f34ff5e7728f
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
wenzelm
parents:
27930
diff
changeset
|
34 |
|
f34ff5e7728f
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
wenzelm
parents:
27930
diff
changeset
|
35 |
def hasNext() = state.isDefined |
f34ff5e7728f
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
wenzelm
parents:
27930
diff
changeset
|
36 |
def next() = state match { |
f34ff5e7728f
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
wenzelm
parents:
27930
diff
changeset
|
37 |
case Some((s, i)) => { state = get_chunk(i); s } |
f34ff5e7728f
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
wenzelm
parents:
27930
diff
changeset
|
38 |
case None => throw new NoSuchElementException("next on empty iterator") |
f34ff5e7728f
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
wenzelm
parents:
27930
diff
changeset
|
39 |
} |
f34ff5e7728f
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
wenzelm
parents:
27930
diff
changeset
|
40 |
} |
f34ff5e7728f
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
wenzelm
parents:
27930
diff
changeset
|
41 |
|
f34ff5e7728f
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
wenzelm
parents:
27930
diff
changeset
|
42 |
|
34099
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
43 |
/* decoding pseudo UTF-8 */ |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
44 |
|
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
45 |
private class Decode_Chars(decode: String => String, |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
46 |
buffer: Array[Byte], start: Int, end: Int) extends CharSequence |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
47 |
{ |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
48 |
def length: Int = end - start |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
49 |
def charAt(i: Int): Char = (buffer(start + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char] |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
50 |
def subSequence(i: Int, j: Int): CharSequence = |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
51 |
new Decode_Chars(decode, buffer, start + i, start + j) |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
52 |
|
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
53 |
// toString with adhoc decoding: abuse of CharSequence interface |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
54 |
// see also http://en.wikipedia.org/wiki/UTF-8#Description |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
55 |
override def toString: String = |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
56 |
{ |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
57 |
val buf = new java.lang.StringBuilder(length) |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
58 |
var code = -1 |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
59 |
var rest = 0 |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
60 |
def flush() |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
61 |
{ |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
62 |
if (code != -1) { |
34118
ee9f87e11400
replace invalid code points -- instead of exception;
wenzelm
parents:
34099
diff
changeset
|
63 |
if (rest == 0 && Character.isValidCodePoint(code)) |
ee9f87e11400
replace invalid code points -- instead of exception;
wenzelm
parents:
34099
diff
changeset
|
64 |
buf.appendCodePoint(code) |
34099
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
65 |
else buf.append('\uFFFD') |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
66 |
code = -1 |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
67 |
rest = 0 |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
68 |
} |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
69 |
} |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
70 |
def init(x: Int, n: Int) |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
71 |
{ |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
72 |
flush() |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
73 |
code = x |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
74 |
rest = n |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
75 |
} |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
76 |
def push(x: Int) |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
77 |
{ |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
78 |
if (rest <= 0) init(x, -1) |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
79 |
else { |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
80 |
code <<= 6 |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
81 |
code += x |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
82 |
rest -= 1 |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
83 |
} |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
84 |
} |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
85 |
for (i <- 0 until length) { |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
86 |
val c = charAt(i) |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
87 |
if (c < 128) { flush(); buf.append(c) } |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
88 |
else if ((c & 0xC0) == 0x80) push(c & 0x3F) |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
89 |
else if ((c & 0xE0) == 0xC0) init(c & 0x1F, 1) |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
90 |
else if ((c & 0xF0) == 0xE0) init(c & 0x0F, 2) |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
91 |
else if ((c & 0xF8) == 0xF0) init(c & 0x07, 3) |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
92 |
} |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
93 |
flush() |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
94 |
decode(buf.toString) |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
95 |
} |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
96 |
} |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
97 |
|
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
98 |
def decode_chars(decode: String => String, |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
99 |
buffer: Array[Byte], start: Int, end: Int): CharSequence = |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
100 |
{ |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
101 |
require(0 <= start && start <= end && end <= buffer.length) |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
102 |
new Decode_Chars(decode, buffer, start, end) |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
103 |
} |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
104 |
|
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
105 |
|
27930 | 106 |
/* parsing */ |
107 |
||
27993
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27971
diff
changeset
|
108 |
private def err(msg: String) = error("Malformed YXML: " + msg) |
27930 | 109 |
private def err_attribute() = err("bad attribute") |
110 |
private def err_element() = err("bad element") |
|
111 |
private def err_unbalanced(name: String) = |
|
112 |
if (name == "") err("unbalanced element") |
|
113 |
else err("unbalanced element \"" + name + "\"") |
|
114 |
||
27944
2bf3f30558ed
parse_attrib: more efficient due to indexOf('=');
wenzelm
parents:
27943
diff
changeset
|
115 |
private def parse_attrib(source: CharSequence) = { |
2bf3f30558ed
parse_attrib: more efficient due to indexOf('=');
wenzelm
parents:
27943
diff
changeset
|
116 |
val s = source.toString |
2bf3f30558ed
parse_attrib: more efficient due to indexOf('=');
wenzelm
parents:
27943
diff
changeset
|
117 |
val i = s.indexOf('=') |
2bf3f30558ed
parse_attrib: more efficient due to indexOf('=');
wenzelm
parents:
27943
diff
changeset
|
118 |
if (i <= 0) err_attribute() |
29563 | 119 |
(s.substring(0, i).intern, s.substring(i + 1)) |
27944
2bf3f30558ed
parse_attrib: more efficient due to indexOf('=');
wenzelm
parents:
27943
diff
changeset
|
120 |
} |
27930 | 121 |
|
122 |
||
32450 | 123 |
def parse_body(source: CharSequence): List[XML.Tree] = |
124 |
{ |
|
27930 | 125 |
/* stack operations */ |
126 |
||
127 |
var stack: List[((String, XML.Attributes), List[XML.Tree])] = null |
|
128 |
||
29180 | 129 |
def add(x: XML.Tree) = (stack: @unchecked) match { |
27930 | 130 |
case ((elem, body) :: pending) => stack = (elem, x :: body) :: pending |
131 |
} |
|
132 |
||
133 |
def push(name: String, atts: XML.Attributes) = |
|
134 |
if (name == "") err_element() |
|
135 |
else stack = ((name, atts), Nil) :: stack |
|
136 |
||
29180 | 137 |
def pop() = (stack: @unchecked) match { |
27930 | 138 |
case ((("", _), _) :: _) => err_unbalanced("") |
139 |
case (((name, atts), body) :: pending) => |
|
140 |
stack = pending; add(XML.Elem(name, atts, body.reverse)) |
|
141 |
} |
|
142 |
||
143 |
||
144 |
/* parse chunks */ |
|
145 |
||
146 |
stack = List((("", Nil), Nil)) |
|
34099
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
147 |
for (chunk <- chunks(X, source) if chunk.length != 0) { |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
148 |
if (chunk.length == 1 && chunk.charAt(0) == Y) pop() |
27945
d2dc5a1903e8
tuned parse performance: avoid splitting terminal Y chunk;
wenzelm
parents:
27944
diff
changeset
|
149 |
else { |
d2dc5a1903e8
tuned parse performance: avoid splitting terminal Y chunk;
wenzelm
parents:
27944
diff
changeset
|
150 |
chunks(Y, chunk).toList match { |
34099
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
151 |
case ch :: name :: atts if ch.length == 0 => |
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
152 |
push(name.toString.intern, atts.map(parse_attrib)) |
27945
d2dc5a1903e8
tuned parse performance: avoid splitting terminal Y chunk;
wenzelm
parents:
27944
diff
changeset
|
153 |
case txts => for (txt <- txts) add(XML.Text(txt.toString)) |
d2dc5a1903e8
tuned parse performance: avoid splitting terminal Y chunk;
wenzelm
parents:
27944
diff
changeset
|
154 |
} |
27930 | 155 |
} |
156 |
} |
|
157 |
stack match { |
|
158 |
case List((("", _), result)) => result.reverse |
|
159 |
case ((name, _), _) :: _ => err_unbalanced(name) |
|
160 |
} |
|
161 |
} |
|
162 |
||
32450 | 163 |
def parse(source: CharSequence): XML.Tree = |
27930 | 164 |
parse_body(source) match { |
165 |
case List(result) => result |
|
166 |
case Nil => XML.Text("") |
|
167 |
case _ => err("multiple results") |
|
168 |
} |
|
27960 | 169 |
|
29521 | 170 |
|
171 |
/* failsafe parsing */ |
|
172 |
||
173 |
private def markup_failsafe(source: CharSequence) = |
|
34119 | 174 |
XML.Elem (Markup.MALFORMED, Nil, |
29521 | 175 |
List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>")))) |
176 |
||
32450 | 177 |
def parse_body_failsafe(source: CharSequence): List[XML.Tree] = |
178 |
{ |
|
29521 | 179 |
try { parse_body(source) } |
180 |
catch { case _: RuntimeException => List(markup_failsafe(source)) } |
|
181 |
} |
|
182 |
||
32450 | 183 |
def parse_failsafe(source: CharSequence): XML.Tree = |
184 |
{ |
|
27960 | 185 |
try { parse(source) } |
29521 | 186 |
catch { case _: RuntimeException => markup_failsafe(source) } |
27960 | 187 |
} |
27930 | 188 |
} |