# HG changeset patch
# User wenzelm
# Date 1310471105 -7200
# Node ID c825594fd0c1e2c3c87452136f60c07acf29e484
# Parent  fc524449f51111eec417ac1f80773a2e5e269298
clarified YXML.embed_controls -- this is idempotent and cannot be nested;

diff -r fc524449f511 -r c825594fd0c1 src/Pure/General/yxml.ML
--- a/src/Pure/General/yxml.ML	Tue Jul 12 13:39:29 2011 +0200
+++ b/src/Pure/General/yxml.ML	Tue Jul 12 13:45:05 2011 +0200
@@ -15,7 +15,7 @@
 
 signature YXML =
 sig
-  val escape_controls: string -> string
+  val embed_controls: string -> string
   val detect: string -> bool
   val output_markup: Markup.T -> string * string
   val element: string -> XML.attributes -> string list -> string
@@ -37,7 +37,7 @@
   then chr 192 ^ chr (128 + ord c)
   else c;
 
-fun escape_controls str =
+fun embed_controls str =
   if exists_string Symbol.is_ascii_control str
   then translate_string pseudo_utf8 str
   else str;
diff -r fc524449f511 -r c825594fd0c1 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Tue Jul 12 13:39:29 2011 +0200
+++ b/src/Pure/System/isabelle_process.ML	Tue Jul 12 13:45:05 2011 +0200
@@ -68,7 +68,7 @@
 
 fun message mbox ch raw_props body =
   let
-    val robust_props = map (pairself YXML.escape_controls) raw_props;
+    val robust_props = map (pairself YXML.embed_controls) raw_props;
     val header = YXML.string_of (XML.Elem ((ch, robust_props), []));
   in Mailbox.send mbox (chunk header @ chunk body) end;