author | wenzelm |
Sun, 04 Sep 2011 15:21:50 +0200 | |
changeset 44698 | 0385292321a0 |
parent 44181 | src/Pure/General/yxml.scala@bbce0417236d |
child 45666 | d83797ef0d2d |
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 |
|
43774
6dfdb70496fe
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents:
43746
diff
changeset
|
18 |
val X = '\5' |
6dfdb70496fe
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents:
43746
diff
changeset
|
19 |
val Y = '\6' |
6dfdb70496fe
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents:
43746
diff
changeset
|
20 |
val X_string = X.toString |
6dfdb70496fe
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents:
43746
diff
changeset
|
21 |
val Y_string = Y.toString |
27930 | 22 |
|
43782 | 23 |
def detect(s: String): Boolean = s.exists(c => c == X || c == Y) |
24 |
||
27930 | 25 |
|
38268
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
26 |
/* string representation */ // FIXME byte array version with pseudo-utf-8 (!?) |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
27 |
|
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
28 |
def string_of_body(body: XML.Body): String = |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
29 |
{ |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
30 |
val s = new StringBuilder |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
31 |
def attrib(p: (String, String)) { s += Y; s ++= p._1; s += '='; s ++= p._2 } |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
32 |
def tree(t: XML.Tree): Unit = |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
33 |
t match { |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
34 |
case XML.Elem(Markup(name, atts), ts) => |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
35 |
s += X; s += Y; s++= name; atts.foreach(attrib); s += X |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
36 |
ts.foreach(tree) |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
37 |
s += X; s += Y; s += X |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
38 |
case XML.Text(text) => s ++= text |
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 |
body.foreach(tree) |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
41 |
s.toString |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
42 |
} |
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
43 |
|
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
44 |
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
|
45 |
|
beb86b805590
more uniform XML/YXML string_of_body/string_of_tree;
wenzelm
parents:
38267
diff
changeset
|
46 |
|
27930 | 47 |
/* parsing */ |
48 |
||
27993
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27971
diff
changeset
|
49 |
private def err(msg: String) = error("Malformed YXML: " + msg) |
27930 | 50 |
private def err_attribute() = err("bad attribute") |
51 |
private def err_element() = err("bad element") |
|
52 |
private def err_unbalanced(name: String) = |
|
53 |
if (name == "") err("unbalanced element") |
|
44181 | 54 |
else err("unbalanced element " + quote(name)) |
27930 | 55 |
|
27944
2bf3f30558ed
parse_attrib: more efficient due to indexOf('=');
wenzelm
parents:
27943
diff
changeset
|
56 |
private def parse_attrib(source: CharSequence) = { |
2bf3f30558ed
parse_attrib: more efficient due to indexOf('=');
wenzelm
parents:
27943
diff
changeset
|
57 |
val s = source.toString |
2bf3f30558ed
parse_attrib: more efficient due to indexOf('=');
wenzelm
parents:
27943
diff
changeset
|
58 |
val i = s.indexOf('=') |
2bf3f30558ed
parse_attrib: more efficient due to indexOf('=');
wenzelm
parents:
27943
diff
changeset
|
59 |
if (i <= 0) err_attribute() |
38234
4b610fbb2d83
YXML.parse: refrain from interning, let XML.Cache do it (partially);
wenzelm
parents:
38231
diff
changeset
|
60 |
(s.substring(0, i), s.substring(i + 1)) |
27944
2bf3f30558ed
parse_attrib: more efficient due to indexOf('=');
wenzelm
parents:
27943
diff
changeset
|
61 |
} |
27930 | 62 |
|
63 |
||
38267
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
38234
diff
changeset
|
64 |
def parse_body(source: CharSequence): XML.Body = |
32450 | 65 |
{ |
27930 | 66 |
/* stack operations */ |
67 |
||
40453 | 68 |
def buffer(): mutable.ListBuffer[XML.Tree] = new mutable.ListBuffer[XML.Tree] |
69 |
var stack: List[(Markup, mutable.ListBuffer[XML.Tree])] = List((Markup.Empty, buffer())) |
|
27930 | 70 |
|
36684 | 71 |
def add(x: XML.Tree) |
72 |
{ |
|
73 |
(stack: @unchecked) match { case ((_, body) :: _) => body += x } |
|
27930 | 74 |
} |
75 |
||
36684 | 76 |
def push(name: String, atts: XML.Attributes) |
77 |
{ |
|
27930 | 78 |
if (name == "") err_element() |
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
36685
diff
changeset
|
79 |
else stack = (Markup(name, atts), buffer()) :: stack |
36684 | 80 |
} |
27930 | 81 |
|
36684 | 82 |
def pop() |
83 |
{ |
|
84 |
(stack: @unchecked) match { |
|
38475 | 85 |
case ((Markup.Empty, _) :: _) => err_unbalanced("") |
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
36685
diff
changeset
|
86 |
case ((markup, body) :: pending) => |
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
36685
diff
changeset
|
87 |
stack = pending |
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
36685
diff
changeset
|
88 |
add(XML.Elem(markup, body.toList)) |
36684 | 89 |
} |
27930 | 90 |
} |
91 |
||
92 |
||
93 |
/* parse chunks */ |
|
94 |
||
36685 | 95 |
for (chunk <- Library.chunks(source, X) 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
|
96 |
if (chunk.length == 1 && chunk.charAt(0) == Y) pop() |
27945
d2dc5a1903e8
tuned parse performance: avoid splitting terminal Y chunk;
wenzelm
parents:
27944
diff
changeset
|
97 |
else { |
36685 | 98 |
Library.chunks(chunk, Y).toList match { |
34099
2541de190d92
added decode_chars, with raw character view on byte buffer and adhoc decoding via toString;
wenzelm
parents:
32450
diff
changeset
|
99 |
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
|
100 |
push(name.toString, atts.map(parse_attrib)) |
27945
d2dc5a1903e8
tuned parse performance: avoid splitting terminal Y chunk;
wenzelm
parents:
27944
diff
changeset
|
101 |
case txts => for (txt <- txts) add(XML.Text(txt.toString)) |
d2dc5a1903e8
tuned parse performance: avoid splitting terminal Y chunk;
wenzelm
parents:
27944
diff
changeset
|
102 |
} |
27930 | 103 |
} |
104 |
} |
|
42719 | 105 |
(stack: @unchecked) match { |
38475 | 106 |
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
|
107 |
case (Markup(name, _), _) :: _ => err_unbalanced(name) |
27930 | 108 |
} |
109 |
} |
|
110 |
||
32450 | 111 |
def parse(source: CharSequence): XML.Tree = |
27930 | 112 |
parse_body(source) match { |
113 |
case List(result) => result |
|
114 |
case Nil => XML.Text("") |
|
115 |
case _ => err("multiple results") |
|
116 |
} |
|
27960 | 117 |
|
29521 | 118 |
|
119 |
/* failsafe parsing */ |
|
120 |
||
43841
60cd0ac63fdb
simplified malformed YXML markup -- special controls are visible in IsabelleText font;
wenzelm
parents:
43782
diff
changeset
|
121 |
private def markup_malformed(source: CharSequence) = |
60cd0ac63fdb
simplified malformed YXML markup -- special controls are visible in IsabelleText font;
wenzelm
parents:
43782
diff
changeset
|
122 |
XML.elem(Markup.MALFORMED, List(XML.Text(source.toString))) |
29521 | 123 |
|
38267
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
38234
diff
changeset
|
124 |
def parse_body_failsafe(source: CharSequence): XML.Body = |
32450 | 125 |
{ |
29521 | 126 |
try { parse_body(source) } |
43841
60cd0ac63fdb
simplified malformed YXML markup -- special controls are visible in IsabelleText font;
wenzelm
parents:
43782
diff
changeset
|
127 |
catch { case ERROR(_) => List(markup_malformed(source)) } |
29521 | 128 |
} |
129 |
||
32450 | 130 |
def parse_failsafe(source: CharSequence): XML.Tree = |
131 |
{ |
|
27960 | 132 |
try { parse(source) } |
43841
60cd0ac63fdb
simplified malformed YXML markup -- special controls are visible in IsabelleText font;
wenzelm
parents:
43782
diff
changeset
|
133 |
catch { case ERROR(_) => markup_malformed(source) } |
27960 | 134 |
} |
27930 | 135 |
} |