Add text_charref to encode a string using character references

--- a/src/Pure/General/xml.ML	Tue Sep 28 10:44:19 2004 +0200
+++ b/src/Pure/General/xml.ML	Tue Sep 28 10:44:51 2004 +0200
@@ -9,6 +9,7 @@
 sig
   val header: string
   val text: string -> string
+  val text_charref: string -> string
   val cdata: string -> string
   val element: string -> (string * string) list -> string list -> string
   datatype tree =
@@ -46,7 +47,11 @@
   | encode "\"" = """
   | encode c = c;
 
-val text = Library.translate_string encode;
+fun encode_charref c = "&#"^Int.toString (Char.ord c)^ ";"
+
+val text = Library.translate_string encode
+
+val text_charref = implode o (map encode_charref) o String.explode
 
 val cdata = enclose "<![CDATA[" "]]>\n"