src/Pure/General/xml.ML

 signature XML =
 sig
   (*string functions*)
   val header: string
   val text: string -> string
-  val text_charref: string -> string
-  val cdata: string -> string
   type attributes = (string * string) list
   val attribute: string * string -> string
   val element: string -> attributes -> string list -> string
   (*tree functions*)
   datatype tree =
       Elem of string * attributes * tree list
     | Text of string
     | Output of output
   type content = tree list
   type element = string * attributes * content
+  val buffer_of_tree: tree -> Buffer.T
   val string_of_tree: tree -> string
-  val buffer_of_tree: tree -> Buffer.T
+  val plain_content: tree -> string
   val parse_string : string -> string option
   val parse_content: string list -> tree list * string list
   val parse_elem: string list -> tree * string list
   val parse_document: string list -> (string option * tree) * string list
   val tree_of_string: string -> tree
-  val scan_comment_whspc : string list -> unit * string list
+  val scan_comment_whspc: string list -> unit * string list
 end;
 
 structure XML: XML =
 struct
 

   | encode "&" = "&"
   | encode "'" = "'"
   | encode "\"" = """
   | encode c = c;
 
-fun encode_charref c = "&#" ^ Int.toString (ord c) ^ ";"
-
-val text = Library.translate_string encode;
-
-val text_charref = translate_string encode_charref;
-
-val cdata = enclose "<![CDATA[" "]]>\n";
+val text = translate_string encode;
 
 
 (* elements *)
 
 fun attribute (a, x) = a ^ " = \"" ^ text x ^ "\"";

     Elem of string * attributes * tree list
   | Text of string
   | Output of output;
 
 type content = tree list;
-
 type element = string * attributes * content;
 
 fun buffer_of_tree tree =
   let
     fun string_of (Elem (name, atts, ts)) buf =

       | string_of (Text s) buf = Buffer.add (text s) buf
       | string_of (Output s) buf = Buffer.add s buf;
   in string_of tree Buffer.empty end;
 
 val string_of_tree = Buffer.content o buffer_of_tree;
+
+fun plain_content tree =
+  let
+    fun content (Elem (_, _, ts)) = fold content ts
+      | content (Text s) = Buffer.add s
+      | content (Output _) = I;    (* FIXME !? *)
+  in Buffer.empty |> content tree |> Buffer.content end;
 
 
 
 (** XML parsing **)