equal
deleted
inserted
replaced
12 |
12 |
13 object YXML |
13 object YXML |
14 { |
14 { |
15 /* chunk markers */ |
15 /* chunk markers */ |
16 |
16 |
17 private val X = '\5' |
17 val X = '\5' |
18 private val Y = '\6' |
18 val Y = '\6' |
19 private val X_string = X.toString |
19 val X_string = X.toString |
20 private val Y_string = Y.toString |
20 val Y_string = Y.toString |
21 |
21 |
22 |
22 |
23 /* string representation */ // FIXME byte array version with pseudo-utf-8 (!?) |
23 /* string representation */ // FIXME byte array version with pseudo-utf-8 (!?) |
24 |
24 |
25 def string_of_body(body: XML.Body): String = |
25 def string_of_body(body: XML.Body): String = |