tuned comments;
authorwenzelm
Thu Apr 03 21:23:38 2008 +0200 (2008-04-03)
changeset 265471112375f6a69
parent 26546 ba4cdf92c7c4
child 26548 41bbcaf3e481
tuned comments;
src/Pure/General/yxml.ML
     1.1 --- a/src/Pure/General/yxml.ML	Thu Apr 03 21:23:37 2008 +0200
     1.2 +++ b/src/Pure/General/yxml.ML	Thu Apr 03 21:23:38 2008 +0200
     1.3 @@ -30,6 +30,8 @@
     1.4  
     1.5  (** string representation **)
     1.6  
     1.7 +(* markers *)
     1.8 +
     1.9  val X = Symbol.ENQ;
    1.10  val Y = Symbol.ACK;
    1.11  val XY = X ^ Y;
    1.12 @@ -38,7 +40,7 @@
    1.13  val detect = String.isPrefix XY;
    1.14  
    1.15  
    1.16 -(* naive pasting of strings *)
    1.17 +(* output *)
    1.18  
    1.19  fun output_markup (name, atts) =
    1.20    (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
    1.21 @@ -47,9 +49,6 @@
    1.22    let val (pre, post) = output_markup (name, atts)
    1.23    in pre ^ implode body ^ post end;
    1.24  
    1.25 -
    1.26 -(* scalable buffer output *)
    1.27 -
    1.28  fun string_of t =
    1.29    let
    1.30      fun attrib (a, x) =