renamed YXML.binary_text to YXML.escape_controls to emphasize what it actually does;

--- a/src/Pure/General/yxml.ML	Tue Aug 10 18:24:16 2010 +0200
+++ b/src/Pure/General/yxml.ML	Tue Aug 10 20:13:52 2010 +0200
@@ -15,7 +15,7 @@
 
 signature YXML =
 sig
-  val binary_text: string -> string
+  val escape_controls: string -> string
   val output_markup: Markup.T -> string * string
   val element: string -> XML.attributes -> string list -> string
   val string_of: XML.tree -> string
@@ -28,14 +28,14 @@
 
 (** string representation **)
 
-(* binary_text -- idempotent recoding *)
+(* idempotent recoding of certain low ASCII control characters *)
 
 fun pseudo_utf8 c =
   if Symbol.is_ascii_control c
   then chr 192 ^ chr (128 + ord c)
   else c;
 
-fun binary_text str =
+fun escape_controls str =
   if exists_string Symbol.is_ascii_control str
   then translate_string pseudo_utf8 str
   else str;

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