eliminated dead code;
authorwenzelm
Wed Mar 07 20:49:18 2012 +0100 (2012-03-07 ago)
changeset 468314a6085849a37
parent 46830 224d01fec36d
child 46832 050e344825c8
eliminated dead code;
tuned;
src/Pure/PIDE/yxml.ML
     1.1 --- a/src/Pure/PIDE/yxml.ML	Wed Mar 07 19:38:36 2012 +0100
     1.2 +++ b/src/Pure/PIDE/yxml.ML	Wed Mar 07 20:49:18 2012 +0100
     1.3 @@ -21,7 +21,6 @@
     1.4    val embed_controls: string -> string
     1.5    val detect: string -> bool
     1.6    val output_markup: Markup.T -> string * string
     1.7 -  val element: string -> XML.attributes -> string list -> string
     1.8    val string_of_body: XML.body -> string
     1.9    val string_of: XML.tree -> string
    1.10    val parse_body: string -> XML.body
    1.11 @@ -62,15 +61,9 @@
    1.12    if Markup.is_empty markup then Markup.no_output
    1.13    else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
    1.14  
    1.15 -fun element name atts body =
    1.16 -  let val (pre, post) = output_markup (name, atts)
    1.17 -  in pre ^ implode body ^ post end;
    1.18 -
    1.19  fun string_of_body body =
    1.20    let
    1.21 -    fun attrib (a, x) =
    1.22 -      Buffer.add Y #>
    1.23 -      Buffer.add a #> Buffer.add "=" #> Buffer.add x;
    1.24 +    fun attrib (a, x) = Buffer.add Y #> Buffer.add a #> Buffer.add "=" #> Buffer.add x;
    1.25      fun tree (XML.Elem ((name, atts), ts)) =
    1.26            Buffer.add XY #> Buffer.add name #> fold attrib atts #> Buffer.add X #>
    1.27            trees ts #>