author | wenzelm |
Mon, 17 May 2021 13:40:01 +0200 | |
changeset 73712 | 3eba8d4b624b |
parent 73556 | 192bcee4f8b8 |
child 75393 | 87ebf5a50283 |
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 |
||
32450 | 14 |
object YXML |
15 |
{ |
|
27943
f34ff5e7728f
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
wenzelm
parents:
27930
diff
changeset
|
16 |
/* chunk markers */ |
27930 | 17 |
|
56661
ef623f6f036b
avoid octal escape literals -- deprecated in scala-2.11.0;
wenzelm
parents:
56600
diff
changeset
|
18 |
val X = '\u0005' |
ef623f6f036b
avoid octal escape literals -- deprecated in scala-2.11.0;
wenzelm
parents:
56600
diff
changeset
|
19 |
val Y = '\u0006' |
56600 | 20 |
|
73029 | 21 |
val is_X: Char => Boolean = _ == X |
22 |
val is_Y: Char => Boolean = _ == Y |
|
56600 | 23 |
|
71601 | 24 |
val X_string: String = X.toString |
25 |
val Y_string: String = Y.toString |
|
26 |
val XY_string: String = X_string + Y_string |
|
27 |
val XYX_string: String = XY_string + X_string |
|
27930 | 28 |
|
43782 | 29 |
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
|
30 |
def detect_elem(s: String): Boolean = s.startsWith(XY_string) |
43782 | 31 |
|
27930 | 32 |
|
73029 | 33 |
/* string representation */ |
38268
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
34 |
|
73340 | 35 |
def traversal(string: String => Unit, body: XML.Body): Unit = |
38268
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
36 |
{ |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
37 |
def tree(t: XML.Tree): Unit = |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
38 |
t match { |
73556
192bcee4f8b8
more robust treatment of empty markup: it allows to produce formal chunks;
wenzelm
parents:
73340
diff
changeset
|
39 |
case XML.Elem(markup @ Markup(name, atts), ts) => |
192bcee4f8b8
more robust treatment of empty markup: it allows to produce formal chunks;
wenzelm
parents:
73340
diff
changeset
|
40 |
if (markup.is_empty) ts.foreach(tree) |
192bcee4f8b8
more robust treatment of empty markup: it allows to produce formal chunks;
wenzelm
parents:
73340
diff
changeset
|
41 |
else { |
192bcee4f8b8
more robust treatment of empty markup: it allows to produce formal chunks;
wenzelm
parents:
73340
diff
changeset
|
42 |
string(XY_string) |
192bcee4f8b8
more robust treatment of empty markup: it allows to produce formal chunks;
wenzelm
parents:
73340
diff
changeset
|
43 |
string(name) |
192bcee4f8b8
more robust treatment of empty markup: it allows to produce formal chunks;
wenzelm
parents:
73340
diff
changeset
|
44 |
for ((a, x) <- atts) { string(Y_string); string(a); string("="); string(x) } |
192bcee4f8b8
more robust treatment of empty markup: it allows to produce formal chunks;
wenzelm
parents:
73340
diff
changeset
|
45 |
string(X_string) |
192bcee4f8b8
more robust treatment of empty markup: it allows to produce formal chunks;
wenzelm
parents:
73340
diff
changeset
|
46 |
ts.foreach(tree) |
192bcee4f8b8
more robust treatment of empty markup: it allows to produce formal chunks;
wenzelm
parents:
73340
diff
changeset
|
47 |
string(XYX_string) |
192bcee4f8b8
more robust treatment of empty markup: it allows to produce formal chunks;
wenzelm
parents:
73340
diff
changeset
|
48 |
} |
71534 | 49 |
case XML.Text(text) => string(text) |
38268
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
50 |
} |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
51 |
body.foreach(tree) |
71534 | 52 |
} |
53 |
||
54 |
def string_of_body(body: XML.Body): String = |
|
55 |
{ |
|
56 |
val s = new StringBuilder |
|
57 |
traversal(str => s ++= str, body) |
|
38268
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
58 |
s.toString |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
59 |
} |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
60 |
|
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
61 |
def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree)) |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
62 |
|
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
63 |
|
27930 | 64 |
/* parsing */ |
65 |
||
27993
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27971
diff
changeset
|
66 |
private def err(msg: String) = error("Malformed YXML: " + msg) |
27930 | 67 |
private def err_attribute() = err("bad attribute") |
68 |
private def err_element() = err("bad element") |
|
69 |
private def err_unbalanced(name: String) = |
|
70 |
if (name == "") err("unbalanced element") |
|
44181 | 71 |
else err("unbalanced element " + quote(name)) |
27930 | 72 |
|
73029 | 73 |
private def parse_attrib(source: CharSequence): (String, String) = |
73712 | 74 |
Properties.Eq.unapply(source.toString) getOrElse err_attribute() |
27930 | 75 |
|
76 |
||
73030 | 77 |
def parse_body(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Body = |
32450 | 78 |
{ |
27930 | 79 |
/* stack operations */ |
80 |
||
40453 | 81 |
def buffer(): mutable.ListBuffer[XML.Tree] = new mutable.ListBuffer[XML.Tree] |
82 |
var stack: List[(Markup, mutable.ListBuffer[XML.Tree])] = List((Markup.Empty, buffer())) |
|
27930 | 83 |
|
73340 | 84 |
def add(x: XML.Tree): Unit = |
73029 | 85 |
(stack: @unchecked) match { case (_, body) :: _ => body += x } |
27930 | 86 |
|
73340 | 87 |
def push(name: String, atts: XML.Attributes): Unit = |
27930 | 88 |
if (name == "") err_element() |
73030 | 89 |
else stack = (cache.markup(Markup(name, atts)), buffer()) :: stack |
27930 | 90 |
|
73340 | 91 |
def pop(): Unit = |
36684 | 92 |
(stack: @unchecked) match { |
73029 | 93 |
case (Markup.Empty, _) :: _ => err_unbalanced("") |
94 |
case (markup, body) :: pending => |
|
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
36685
diff
changeset
|
95 |
stack = pending |
73030 | 96 |
add(cache.tree0(XML.Elem(markup, body.toList))) |
36684 | 97 |
} |
27930 | 98 |
|
99 |
||
100 |
/* parse chunks */ |
|
101 |
||
56600 | 102 |
for (chunk <- Library.separated_chunks(is_X, source) if chunk.length != 0) { |
34099
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
103 |
if (chunk.length == 1 && chunk.charAt(0) == Y) pop() |
27945
d2dc5a1903e8
tuned parse performance: avoid splitting terminal Y chunk;
wenzelm
parents:
27944
diff
changeset
|
104 |
else { |
56600 | 105 |
Library.separated_chunks(is_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
|
106 |
case ch :: name :: atts if ch.length == 0 => |
38234
4b610fbb2d83
YXML.parse: refrain from interning, let XML.Cache do it (partially);
wenzelm
parents:
38231
diff
changeset
|
107 |
push(name.toString, atts.map(parse_attrib)) |
73030 | 108 |
case txts => for (txt <- txts) add(cache.tree0(XML.Text(cache.string(txt.toString)))) |
27945
d2dc5a1903e8
tuned parse performance: avoid splitting terminal Y chunk;
wenzelm
parents:
27944
diff
changeset
|
109 |
} |
27930 | 110 |
} |
111 |
} |
|
42719 | 112 |
(stack: @unchecked) match { |
38475 | 113 |
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
|
114 |
case (Markup(name, _), _) :: _ => err_unbalanced(name) |
27930 | 115 |
} |
116 |
} |
|
117 |
||
73030 | 118 |
def parse(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Tree = |
119 |
parse_body(source, cache = cache) match { |
|
27930 | 120 |
case List(result) => result |
73028 | 121 |
case Nil => XML.no_text |
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
64370
diff
changeset
|
122 |
case _ => err("multiple XML trees") |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
64370
diff
changeset
|
123 |
} |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
64370
diff
changeset
|
124 |
|
73030 | 125 |
def parse_elem(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Tree = |
126 |
parse_body(source, cache = cache) match { |
|
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
64370
diff
changeset
|
127 |
case List(elem: XML.Elem) => elem |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
64370
diff
changeset
|
128 |
case _ => err("single XML element expected") |
27930 | 129 |
} |
27960 | 130 |
|
29521 | 131 |
|
132 |
/* failsafe parsing */ |
|
133 |
||
45666 | 134 |
private def markup_broken(source: CharSequence) = |
55551 | 135 |
XML.Elem(Markup.Broken, List(XML.Text(source.toString))) |
29521 | 136 |
|
73030 | 137 |
def parse_body_failsafe(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Body = |
32450 | 138 |
{ |
73030 | 139 |
try { parse_body(source, cache = cache) } |
45666 | 140 |
catch { case ERROR(_) => List(markup_broken(source)) } |
29521 | 141 |
} |
142 |
||
73030 | 143 |
def parse_failsafe(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Tree = |
32450 | 144 |
{ |
73030 | 145 |
try { parse(source, cache = cache) } |
45666 | 146 |
catch { case ERROR(_) => markup_broken(source) } |
27960 | 147 |
} |
27930 | 148 |
} |