# HG changeset patch
# User aspinall
# Date 1096361091 -7200
# Node ID 5f54721547a7b42e5af044814e6f5e0b98e55fd8
# Parent  4ff917a91e1618a1bcd569260099b0521bea9a20
Add text_charref to encode a string using character references

diff -r 4ff917a91e16 -r 5f54721547a7 src/Pure/General/xml.ML
--- 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"