| changeset 45667 | 546d78f0d81f |
| parent 45666 | d83797ef0d2d |
| child 45673 | cd41e3903fbf |
| 45666:d83797ef0d2d | 45667:546d78f0d81f |
|---|---|
1 /* Title: Pure/PIDE/yxml.scala |
1 /* Title: Pure/PIDE/yxml.scala |
2 Module: Library |
|
2 Author: Makarius |
3 Author: Makarius |
3 |
4 |
4 Efficient text representation of XML trees. Suitable for direct |
5 Efficient text representation of XML trees. Suitable for direct |
5 inlining into plain text. |
6 inlining into plain text. |
6 */ |
7 */ |