1.1 --- a/src/Pure/General/yxml.ML	Tue Jul 12 13:39:29 2011 +0200
     1.2 +++ b/src/Pure/General/yxml.ML	Tue Jul 12 13:45:05 2011 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  
     1.5  signature YXML =
     1.6  sig
     1.7 -  val escape_controls: string -> string
     1.8 +  val embed_controls: string -> string
     1.9    val detect: string -> bool
    1.10    val output_markup: Markup.T -> string * string
    1.11    val element: string -> XML.attributes -> string list -> string
    1.12 @@ -37,7 +37,7 @@
    1.13    then chr 192 ^ chr (128 + ord c)
    1.14    else c;
    1.15  
    1.16 -fun escape_controls str =
    1.17 +fun embed_controls str =
    1.18    if exists_string Symbol.is_ascii_control str
    1.19    then translate_string pseudo_utf8 str
    1.20    else str;

     2.1 --- a/src/Pure/System/isabelle_process.ML	Tue Jul 12 13:39:29 2011 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.ML	Tue Jul 12 13:45:05 2011 +0200
     2.3 @@ -68,7 +68,7 @@
     2.4  
     2.5  fun message mbox ch raw_props body =
     2.6    let
     2.7 -    val robust_props = map (pairself YXML.escape_controls) raw_props;
     2.8 +    val robust_props = map (pairself YXML.embed_controls) raw_props;
     2.9      val header = YXML.string_of (XML.Elem ((ch, robust_props), []));
    2.10    in Mailbox.send mbox (chunk header @ chunk body) end;
    2.11