src/Pure/General/yxml.ML
changeset 26547 1112375f6a69
parent 26540 173d548ce9d2
child 26684 0701201def95
equal deleted inserted replaced
26546:ba4cdf92c7c4 26547:1112375f6a69
    28 structure YXML: YXML =
    28 structure YXML: YXML =
    29 struct
    29 struct
    30 
    30 
    31 (** string representation **)
    31 (** string representation **)
    32 
    32 
       
    33 (* markers *)
       
    34 
    33 val X = Symbol.ENQ;
    35 val X = Symbol.ENQ;
    34 val Y = Symbol.ACK;
    36 val Y = Symbol.ACK;
    35 val XY = X ^ Y;
    37 val XY = X ^ Y;
    36 val XYX = XY ^ X;
    38 val XYX = XY ^ X;
    37 
    39 
    38 val detect = String.isPrefix XY;
    40 val detect = String.isPrefix XY;
    39 
    41 
    40 
    42 
    41 (* naive pasting of strings *)
    43 (* output *)
    42 
    44 
    43 fun output_markup (name, atts) =
    45 fun output_markup (name, atts) =
    44   (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
    46   (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
    45 
    47 
    46 fun element name atts body =
    48 fun element name atts body =
    47   let val (pre, post) = output_markup (name, atts)
    49   let val (pre, post) = output_markup (name, atts)
    48   in pre ^ implode body ^ post end;
    50   in pre ^ implode body ^ post end;
    49 
       
    50 
       
    51 (* scalable buffer output *)
       
    52 
    51 
    53 fun string_of t =
    52 fun string_of t =
    54   let
    53   let
    55     fun attrib (a, x) =
    54     fun attrib (a, x) =
    56       Buffer.add Y #>
    55       Buffer.add Y #>