Add text_charref to encode a string using character references
authoraspinall
Tue Sep 28 10:44:51 2004 +0200 (2004-09-28)
changeset 152115f54721547a7
parent 15210 4ff917a91e16
child 15212 eb4343a0d571
Add text_charref to encode a string using character references
src/Pure/General/xml.ML
     1.1 --- a/src/Pure/General/xml.ML	Tue Sep 28 10:44:19 2004 +0200
     1.2 +++ b/src/Pure/General/xml.ML	Tue Sep 28 10:44:51 2004 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  sig
     1.5    val header: string
     1.6    val text: string -> string
     1.7 +  val text_charref: string -> string
     1.8    val cdata: string -> string
     1.9    val element: string -> (string * string) list -> string list -> string
    1.10    datatype tree =
    1.11 @@ -46,7 +47,11 @@
    1.12    | encode "\"" = """
    1.13    | encode c = c;
    1.14  
    1.15 -val text = Library.translate_string encode;
    1.16 +fun encode_charref c = "&#"^Int.toString (Char.ord c)^ ";"
    1.17 +
    1.18 +val text = Library.translate_string encode
    1.19 +
    1.20 +val text_charref = implode o (map encode_charref) o String.explode
    1.21  
    1.22  val cdata = enclose "<![CDATA[" "]]>\n"
    1.23