--- a/src/Pure/PIDE/yxml.scala Tue Apr 22 23:01:59 2014 +0200
+++ b/src/Pure/PIDE/yxml.scala Tue Apr 22 23:31:45 2014 +0200
@@ -16,8 +16,8 @@
{
/* chunk markers */
- val X = '\5'
- val Y = '\6'
+ val X = '\u0005'
+ val Y = '\u0006'
val is_X = (c: Char) => c == X
val is_Y = (c: Char) => c == Y