author | wenzelm |
Tue, 02 Jul 2024 23:13:35 +0200 | |
changeset 80480 | 972f7a4cdc0e |
parent 80447 | 325907d85977 |
child 80486 | 24290f18ceb1 |
permissions | -rw-r--r-- |
44698 | 1 |
/* Title: Pure/PIDE/yxml.scala |
27930 | 2 |
Author: Makarius |
3 |
||
44698 | 4 |
Efficient text representation of XML trees. Suitable for direct |
5 |
inlining into plain text. |
|
27930 | 6 |
*/ |
7 |
||
8 |
package isabelle |
|
9 |
||
10 |
||
40453 | 11 |
import scala.collection.mutable |
36684 | 12 |
|
13 |
||
75393 | 14 |
object YXML { |
27943
f34ff5e7728f
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
wenzelm
parents:
27930
diff
changeset
|
15 |
/* chunk markers */ |
27930 | 16 |
|
80425 | 17 |
val X_byte: Byte = 5 |
18 |
val Y_byte: Byte = 6 |
|
19 |
||
20 |
val X = X_byte.toChar |
|
21 |
val Y = Y_byte.toChar |
|
56600 | 22 |
|
73029 | 23 |
val is_X: Char => Boolean = _ == X |
24 |
val is_Y: Char => Boolean = _ == Y |
|
56600 | 25 |
|
71601 | 26 |
val X_string: String = X.toString |
27 |
val Y_string: String = Y.toString |
|
28 |
val XY_string: String = X_string + Y_string |
|
29 |
val XYX_string: String = XY_string + X_string |
|
27930 | 30 |
|
43782 | 31 |
def detect(s: String): Boolean = s.exists(c => c == X || c == Y) |
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
64370
diff
changeset
|
32 |
def detect_elem(s: String): Boolean = s.startsWith(XY_string) |
43782 | 33 |
|
27930 | 34 |
|
73029 | 35 |
/* string representation */ |
38268
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
36 |
|
80433
48776d779d94
more robust: prefer tail-recursive XML.Traversal;
wenzelm
parents:
80427
diff
changeset
|
37 |
trait Output extends XML.Traversal { |
80425 | 38 |
def byte(b: Byte): Unit |
39 |
def string(s: String): Unit |
|
80433
48776d779d94
more robust: prefer tail-recursive XML.Traversal;
wenzelm
parents:
80427
diff
changeset
|
40 |
|
48776d779d94
more robust: prefer tail-recursive XML.Traversal;
wenzelm
parents:
80427
diff
changeset
|
41 |
// XML.Traversal |
48776d779d94
more robust: prefer tail-recursive XML.Traversal;
wenzelm
parents:
80427
diff
changeset
|
42 |
override def text(s: String): Unit = string(s) |
48776d779d94
more robust: prefer tail-recursive XML.Traversal;
wenzelm
parents:
80427
diff
changeset
|
43 |
override def elem(markup: Markup, end: Boolean = false): Unit = { |
48776d779d94
more robust: prefer tail-recursive XML.Traversal;
wenzelm
parents:
80427
diff
changeset
|
44 |
byte(X_byte) |
48776d779d94
more robust: prefer tail-recursive XML.Traversal;
wenzelm
parents:
80427
diff
changeset
|
45 |
byte(Y_byte) |
48776d779d94
more robust: prefer tail-recursive XML.Traversal;
wenzelm
parents:
80427
diff
changeset
|
46 |
string(markup.name) |
48776d779d94
more robust: prefer tail-recursive XML.Traversal;
wenzelm
parents:
80427
diff
changeset
|
47 |
for ((a, b) <- markup.properties) { |
48776d779d94
more robust: prefer tail-recursive XML.Traversal;
wenzelm
parents:
80427
diff
changeset
|
48 |
byte(Y_byte) |
48776d779d94
more robust: prefer tail-recursive XML.Traversal;
wenzelm
parents:
80427
diff
changeset
|
49 |
string(a) |
48776d779d94
more robust: prefer tail-recursive XML.Traversal;
wenzelm
parents:
80427
diff
changeset
|
50 |
byte('='.toByte) |
48776d779d94
more robust: prefer tail-recursive XML.Traversal;
wenzelm
parents:
80427
diff
changeset
|
51 |
string(b) |
38268
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
52 |
} |
80433
48776d779d94
more robust: prefer tail-recursive XML.Traversal;
wenzelm
parents:
80427
diff
changeset
|
53 |
byte(X_byte) |
48776d779d94
more robust: prefer tail-recursive XML.Traversal;
wenzelm
parents:
80427
diff
changeset
|
54 |
if (end) end_elem(markup.name) |
48776d779d94
more robust: prefer tail-recursive XML.Traversal;
wenzelm
parents:
80427
diff
changeset
|
55 |
} |
48776d779d94
more robust: prefer tail-recursive XML.Traversal;
wenzelm
parents:
80427
diff
changeset
|
56 |
override def end_elem(name: String): Unit = { |
48776d779d94
more robust: prefer tail-recursive XML.Traversal;
wenzelm
parents:
80427
diff
changeset
|
57 |
byte(X_byte) |
48776d779d94
more robust: prefer tail-recursive XML.Traversal;
wenzelm
parents:
80427
diff
changeset
|
58 |
byte(Y_byte) |
48776d779d94
more robust: prefer tail-recursive XML.Traversal;
wenzelm
parents:
80427
diff
changeset
|
59 |
byte(X_byte) |
48776d779d94
more robust: prefer tail-recursive XML.Traversal;
wenzelm
parents:
80427
diff
changeset
|
60 |
} |
71534 | 61 |
} |
62 |
||
80437
2c07b9b2f9f4
minor performance tuning: more direct Bytes with Symbol.encode;
wenzelm
parents:
80433
diff
changeset
|
63 |
class Output_String(builder: StringBuilder, recode: String => String = identity) extends Output { |
80425 | 64 |
override def byte(b: Byte): Unit = { builder += b.toChar } |
80437
2c07b9b2f9f4
minor performance tuning: more direct Bytes with Symbol.encode;
wenzelm
parents:
80433
diff
changeset
|
65 |
override def string(s: String): Unit = { builder ++= recode(s) } |
80433
48776d779d94
more robust: prefer tail-recursive XML.Traversal;
wenzelm
parents:
80427
diff
changeset
|
66 |
def result(ts: List[XML.Tree]): String = { traverse(ts); builder.toString } |
38268
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
67 |
} |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
68 |
|
80437
2c07b9b2f9f4
minor performance tuning: more direct Bytes with Symbol.encode;
wenzelm
parents:
80433
diff
changeset
|
69 |
class Output_Bytes(builder: Bytes.Builder, recode: String => String = identity) extends Output { |
80427 | 70 |
override def byte(b: Byte): Unit = { builder += b } |
80437
2c07b9b2f9f4
minor performance tuning: more direct Bytes with Symbol.encode;
wenzelm
parents:
80433
diff
changeset
|
71 |
override def string(s: String): Unit = { builder += recode(s) } |
80427 | 72 |
} |
73 |
||
80437
2c07b9b2f9f4
minor performance tuning: more direct Bytes with Symbol.encode;
wenzelm
parents:
80433
diff
changeset
|
74 |
def string_of_body(body: XML.Body, recode: String => String = identity): String = |
2c07b9b2f9f4
minor performance tuning: more direct Bytes with Symbol.encode;
wenzelm
parents:
80433
diff
changeset
|
75 |
new Output_String(new StringBuilder, recode = recode).result(body) |
80425 | 76 |
|
80437
2c07b9b2f9f4
minor performance tuning: more direct Bytes with Symbol.encode;
wenzelm
parents:
80433
diff
changeset
|
77 |
def string_of_tree(tree: XML.Tree, recode: String => String = identity): String = |
2c07b9b2f9f4
minor performance tuning: more direct Bytes with Symbol.encode;
wenzelm
parents:
80433
diff
changeset
|
78 |
string_of_body(List(tree), recode = recode) |
38268
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
79 |
|
80437
2c07b9b2f9f4
minor performance tuning: more direct Bytes with Symbol.encode;
wenzelm
parents:
80433
diff
changeset
|
80 |
def bytes_of_body(body: XML.Body, recode: String => String = identity): Bytes = |
2c07b9b2f9f4
minor performance tuning: more direct Bytes with Symbol.encode;
wenzelm
parents:
80433
diff
changeset
|
81 |
Bytes.Builder.use()(builder => new Output_Bytes(builder, recode = recode).traverse(body)) |
80427 | 82 |
|
80437
2c07b9b2f9f4
minor performance tuning: more direct Bytes with Symbol.encode;
wenzelm
parents:
80433
diff
changeset
|
83 |
def bytes_of_tree(tree: XML.Tree, recode: String => String = identity): Bytes = |
2c07b9b2f9f4
minor performance tuning: more direct Bytes with Symbol.encode;
wenzelm
parents:
80433
diff
changeset
|
84 |
bytes_of_body(List(tree), recode = recode) |
80427 | 85 |
|
38268
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
86 |
|
27930 | 87 |
/* parsing */ |
88 |
||
27993
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27971
diff
changeset
|
89 |
private def err(msg: String) = error("Malformed YXML: " + msg) |
27930 | 90 |
private def err_attribute() = err("bad attribute") |
91 |
private def err_element() = err("bad element") |
|
92 |
private def err_unbalanced(name: String) = |
|
93 |
if (name == "") err("unbalanced element") |
|
44181 | 94 |
else err("unbalanced element " + quote(name)) |
27930 | 95 |
|
80480
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
96 |
object Source { |
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
97 |
def apply(s: String): Source = new Source_String(s) |
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
98 |
} |
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
99 |
|
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
100 |
trait Source { |
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
101 |
def is_empty: Boolean |
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
102 |
def is_X: Boolean |
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
103 |
def is_Y: Boolean |
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
104 |
def iterator_X: Iterator[Source] |
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
105 |
def iterator_Y: Iterator[Source] |
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
106 |
def text: String |
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
107 |
} |
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
108 |
|
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
109 |
class Source_String(source: String) extends Source { |
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
110 |
override def is_empty: Boolean = source.isEmpty |
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
111 |
override def is_X: Boolean = source.length == 1 && source(0) == X |
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
112 |
override def is_Y: Boolean = source.length == 1 && source(0) == Y |
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
113 |
override def iterator_X: Iterator[Source] = |
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
114 |
Library.separated_chunks(X, source).map(Source.apply) |
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
115 |
override def iterator_Y: Iterator[Source] = |
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
116 |
Library.separated_chunks(Y, source).map(Source.apply) |
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
117 |
override def text: String = source |
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
118 |
} |
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
119 |
|
80447
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
120 |
def parse_body( |
80480
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
121 |
source: Source, |
80447
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
122 |
recode: String => String = identity, |
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
123 |
cache: XML.Cache = XML.Cache.none |
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
124 |
): XML.Body = { |
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
125 |
/* parse + recode */ |
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
126 |
|
80480
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
127 |
def parse_string(s: Source): String = recode(s.text) |
80447
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
128 |
|
80480
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
129 |
def parse_attrib(s: Source): (String, String) = |
80447
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
130 |
Properties.Eq.unapply(parse_string(s)) getOrElse err_attribute() |
27930 | 131 |
|
132 |
||
133 |
/* stack operations */ |
|
134 |
||
40453 | 135 |
def buffer(): mutable.ListBuffer[XML.Tree] = new mutable.ListBuffer[XML.Tree] |
136 |
var stack: List[(Markup, mutable.ListBuffer[XML.Tree])] = List((Markup.Empty, buffer())) |
|
27930 | 137 |
|
73340 | 138 |
def add(x: XML.Tree): Unit = |
73029 | 139 |
(stack: @unchecked) match { case (_, body) :: _ => body += x } |
27930 | 140 |
|
73340 | 141 |
def push(name: String, atts: XML.Attributes): Unit = |
27930 | 142 |
if (name == "") err_element() |
73030 | 143 |
else stack = (cache.markup(Markup(name, atts)), buffer()) :: stack |
27930 | 144 |
|
73340 | 145 |
def pop(): Unit = |
36684 | 146 |
(stack: @unchecked) match { |
73029 | 147 |
case (Markup.Empty, _) :: _ => err_unbalanced("") |
148 |
case (markup, body) :: pending => |
|
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
36685
diff
changeset
|
149 |
stack = pending |
73030 | 150 |
add(cache.tree0(XML.Elem(markup, body.toList))) |
36684 | 151 |
} |
27930 | 152 |
|
153 |
||
154 |
/* parse chunks */ |
|
155 |
||
80480
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
156 |
for (chunk <- source.iterator_X if !chunk.is_empty) { |
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
157 |
if (chunk.is_Y) pop() |
27945
d2dc5a1903e8
tuned parse performance: avoid splitting terminal Y chunk;
wenzelm
parents:
27944
diff
changeset
|
158 |
else { |
80480
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
159 |
chunk.iterator_Y.toList match { |
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
160 |
case ch :: name :: atts if ch.is_empty => |
80447
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
161 |
push(parse_string(name), atts.map(parse_attrib)) |
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
162 |
case txts => |
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
163 |
for (txt <- txts) add(cache.tree0(XML.Text(cache.string(parse_string(txt))))) |
27945
d2dc5a1903e8
tuned parse performance: avoid splitting terminal Y chunk;
wenzelm
parents:
27944
diff
changeset
|
164 |
} |
27930 | 165 |
} |
166 |
} |
|
42719 | 167 |
(stack: @unchecked) match { |
38475 | 168 |
case List((Markup.Empty, body)) => body.toList |
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
36685
diff
changeset
|
169 |
case (Markup(name, _), _) :: _ => err_unbalanced(name) |
27930 | 170 |
} |
171 |
} |
|
172 |
||
80447
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
173 |
def parse( |
80480
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
174 |
source: Source, |
80447
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
175 |
recode: String => String = identity, |
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
176 |
cache: XML.Cache = XML.Cache.none |
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
177 |
): XML.Tree = |
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
178 |
parse_body(source, recode = recode, cache = cache) match { |
27930 | 179 |
case List(result) => result |
73028 | 180 |
case Nil => XML.no_text |
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
64370
diff
changeset
|
181 |
case _ => err("multiple XML trees") |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
64370
diff
changeset
|
182 |
} |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
64370
diff
changeset
|
183 |
|
80447
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
184 |
def parse_elem( |
80480
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
185 |
source: Source, |
80447
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
186 |
recode: String => String = identity, |
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
187 |
cache: XML.Cache = XML.Cache.none |
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
188 |
): XML.Tree = |
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
189 |
parse_body(source, recode = recode, cache = cache) match { |
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
64370
diff
changeset
|
190 |
case List(elem: XML.Elem) => elem |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
64370
diff
changeset
|
191 |
case _ => err("single XML element expected") |
27930 | 192 |
} |
27960 | 193 |
|
29521 | 194 |
|
195 |
/* failsafe parsing */ |
|
196 |
||
80480
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
197 |
private def markup_broken(source: Source) = |
55551 | 198 |
XML.Elem(Markup.Broken, List(XML.Text(source.toString))) |
29521 | 199 |
|
80447
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
200 |
def parse_body_failsafe( |
80480
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
201 |
source: Source, |
80447
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
202 |
recode: String => String = identity, |
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
203 |
cache: XML.Cache = XML.Cache.none |
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
204 |
): XML.Body = { |
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
205 |
try { parse_body(source, recode = recode, cache = cache) } |
45666 | 206 |
catch { case ERROR(_) => List(markup_broken(source)) } |
29521 | 207 |
} |
208 |
||
80447
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
209 |
def parse_failsafe( |
80480
972f7a4cdc0e
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents:
80447
diff
changeset
|
210 |
source: Source, |
80447
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
211 |
recode: String => String = identity, |
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
212 |
cache: XML.Cache = XML.Cache.none |
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
213 |
): XML.Tree = { |
325907d85977
minor performance tuning: allow recode operation during YXML parsing;
wenzelm
parents:
80437
diff
changeset
|
214 |
try { parse(source, recode = recode, cache = cache) } |
45666 | 215 |
catch { case ERROR(_) => markup_broken(source) } |
27960 | 216 |
} |
27930 | 217 |
} |