src/Pure/General/yxml.ML
changeset 38265 cc9fde54311f
parent 38228 ada3ab6b9085
child 38266 492d377ecfe2
     1.1 --- a/src/Pure/General/yxml.ML	Tue Aug 10 18:24:16 2010 +0200
     1.2 +++ b/src/Pure/General/yxml.ML	Tue Aug 10 20:13:52 2010 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  
     1.5  signature YXML =
     1.6  sig
     1.7 -  val binary_text: string -> string
     1.8 +  val escape_controls: string -> string
     1.9    val output_markup: Markup.T -> string * string
    1.10    val element: string -> XML.attributes -> string list -> string
    1.11    val string_of: XML.tree -> string
    1.12 @@ -28,14 +28,14 @@
    1.13  
    1.14  (** string representation **)
    1.15  
    1.16 -(* binary_text -- idempotent recoding *)
    1.17 +(* idempotent recoding of certain low ASCII control characters *)
    1.18  
    1.19  fun pseudo_utf8 c =
    1.20    if Symbol.is_ascii_control c
    1.21    then chr 192 ^ chr (128 + ord c)
    1.22    else c;
    1.23  
    1.24 -fun binary_text str =
    1.25 +fun escape_controls str =
    1.26    if exists_string Symbol.is_ascii_control str
    1.27    then translate_string pseudo_utf8 str
    1.28    else str;