# HG changeset patch
# User wenzelm
# Date 1219876389 -7200
# Node ID f03b5856f2865307d6a2aa5da7321d4fa440e0ec
# Parent  cb0021c989cd872d7efc10f4ebf8dc3dd8c4cbe9
removed obsolete XML.Output workaround;

diff -r cb0021c989cd -r f03b5856f286 src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Thu Aug 28 00:33:08 2008 +0200
+++ b/src/Pure/General/xml.ML	Thu Aug 28 00:33:09 2008 +0200
@@ -11,7 +11,6 @@
   datatype tree =
       Elem of string * attributes * tree list
     | Text of string
-    | Output of output
   val add_content: tree -> Buffer.T -> Buffer.T
   val detect: string -> bool
   val header: string
@@ -36,12 +35,10 @@
 
 datatype tree =
     Elem of string * attributes * tree list
-  | Text of string
-  | Output of output;   (* FIXME !? *)
+  | Text of string;
 
 fun add_content (Elem (_, _, ts)) = fold add_content ts
-  | add_content (Text s) = Buffer.add s
-  | add_content (Output _) = I;    (* FIXME !? *)
+  | add_content (Text s) = Buffer.add s;
 
 
 
@@ -96,8 +93,7 @@
           Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add ">" #>
           fold traverse ts #>
           Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
-      | traverse (Text s) = Buffer.add (text s)
-      | traverse (Output s) = Buffer.add s;
+      | traverse (Text s) = Buffer.add (text s);
   in Buffer.empty |> traverse tree end;
 
 val string_of = Buffer.content o buffer_of;
diff -r cb0021c989cd -r f03b5856f286 src/Pure/General/yxml.ML
--- a/src/Pure/General/yxml.ML	Thu Aug 28 00:33:08 2008 +0200
+++ b/src/Pure/General/yxml.ML	Thu Aug 28 00:33:09 2008 +0200
@@ -58,8 +58,7 @@
           Buffer.add XY #> Buffer.add name #> fold attrib atts #> Buffer.add X #>
           fold tree ts #>
           Buffer.add XYX
-      | tree (XML.Text s) = Buffer.add s
-      | tree (XML.Output s) = Buffer.add s;
+      | tree (XML.Text s) = Buffer.add s;
   in Buffer.empty |> tree t |> Buffer.content end;