--- a/src/Pure/General/yxml.ML Thu Apr 03 21:23:37 2008 +0200
+++ b/src/Pure/General/yxml.ML Thu Apr 03 21:23:38 2008 +0200
@@ -30,6 +30,8 @@
(** string representation **)
+(* markers *)
+
val X = Symbol.ENQ;
val Y = Symbol.ACK;
val XY = X ^ Y;
@@ -38,7 +40,7 @@
val detect = String.isPrefix XY;
-(* naive pasting of strings *)
+(* output *)
fun output_markup (name, atts) =
(XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
@@ -47,9 +49,6 @@
let val (pre, post) = output_markup (name, atts)
in pre ^ implode body ^ post end;
-
-(* scalable buffer output *)
-
fun string_of t =
let
fun attrib (a, x) =