changeset 31521 | 73adb1fa8553 |
parent 31469 | 40f815edbde4 |
child 32450 | 375db037f4d2 |
31520:0a99c8716312 | 31521:73adb1fa8553 |
---|---|
3 |
3 |
4 Efficient text representation of XML trees. |
4 Efficient text representation of XML trees. |
5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
|
9 import java.util.regex.Pattern |
|
10 |
8 |
11 |
9 |
12 object YXML { |
10 object YXML { |
13 |
11 |
14 /* chunk markers */ |
12 /* chunk markers */ |