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;

     2.1 --- a/src/Pure/System/isabelle_process.ML	Tue Aug 10 18:24:16 2010 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.ML	Tue Aug 10 20:13:52 2010 +0200
     2.3 @@ -34,7 +34,7 @@
     2.4  fun message _ _ _ "" = ()
     2.5    | message out_stream ch props body =
     2.6        let
     2.7 -        val header = YXML.string_of (XML.Elem ((ch, map (pairself YXML.binary_text) props), []));
     2.8 +        val header = YXML.string_of (XML.Elem ((ch, map (pairself YXML.escape_controls) props), []));
     2.9          val msg = Symbol.STX ^ chunk header ^ chunk body;
    2.10        in TextIO.output (out_stream, msg) (*atomic output*) end;
    2.11