changeset 43777 | 22c87ff1b8a9 |
parent 43772 | c825594fd0c1 |
child 43782 | 834de29572d5 |
--- a/src/Pure/General/yxml.ML Tue Jul 12 15:17:37 2011 +0200 +++ b/src/Pure/General/yxml.ML Tue Jul 12 15:32:16 2011 +0200 @@ -15,6 +15,8 @@ signature YXML = sig + val X: Symbol.symbol + val Y: Symbol.symbol val embed_controls: string -> string val detect: string -> bool val output_markup: Markup.T -> string * string @@ -45,8 +47,8 @@ (* markers *) -val X = Symbol.ENQ; -val Y = Symbol.ACK; +val X = chr 5; +val Y = chr 6; val XY = X ^ Y; val XYX = XY ^ X;