--- a/src/Pure/General/yxml.ML Wed Dec 16 15:15:39 2009 +0100
+++ b/src/Pure/General/yxml.ML Thu Dec 17 13:58:15 2009 +0100
@@ -15,6 +15,7 @@
signature YXML =
sig
+ val binary_text: string -> string
val output_markup: Markup.T -> string * string
val element: string -> XML.attributes -> string list -> string
val string_of: XML.tree -> string
@@ -27,6 +28,19 @@
(** string representation **)
+(* binary_text -- idempotent recoding *)
+
+fun pseudo_utf8 c =
+ if Symbol.is_ascii_control c
+ then chr 192 ^ chr (128 + ord c)
+ else c;
+
+fun binary_text str =
+ if exists_string Symbol.is_ascii_control str
+ then translate_string pseudo_utf8 str
+ else str;
+
+
(* markers *)
val X = Symbol.ENQ;