# HG changeset patch
# User wenzelm
# Date 1207250618 -7200
# Node ID 1112375f6a692c6166818eabb06e3633b0fcda66
# Parent  ba4cdf92c7c4f99925b2ed008bb136578999ce27
tuned comments;

diff -r ba4cdf92c7c4 -r 1112375f6a69 src/Pure/General/yxml.ML
--- 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) =