# HG changeset patch
# User wenzelm
# Date 1331149758 -3600
# Node ID 4a6085849a37fa7d57f5a447ecd43ef422808146
# Parent  224d01fec36d5693fcc85c4efbc776214b0b8778
eliminated dead code;
tuned;

diff -r 224d01fec36d -r 4a6085849a37 src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Wed Mar 07 19:38:36 2012 +0100
+++ b/src/Pure/PIDE/yxml.ML	Wed Mar 07 20:49:18 2012 +0100
@@ -21,7 +21,6 @@
   val embed_controls: string -> string
   val detect: string -> bool
   val output_markup: Markup.T -> string * string
-  val element: string -> XML.attributes -> string list -> string
   val string_of_body: XML.body -> string
   val string_of: XML.tree -> string
   val parse_body: string -> XML.body
@@ -62,15 +61,9 @@
   if Markup.is_empty markup then Markup.no_output
   else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
 
-fun element name atts body =
-  let val (pre, post) = output_markup (name, atts)
-  in pre ^ implode body ^ post end;
-
 fun string_of_body body =
   let
-    fun attrib (a, x) =
-      Buffer.add Y #>
-      Buffer.add a #> Buffer.add "=" #> Buffer.add x;
+    fun attrib (a, x) = Buffer.add Y #> Buffer.add a #> Buffer.add "=" #> Buffer.add x;
     fun tree (XML.Elem ((name, atts), ts)) =
           Buffer.add XY #> Buffer.add name #> fold attrib atts #> Buffer.add X #>
           trees ts #>