added escape_malformed (failsafe);

--- a/src/Pure/General/output.ML	Tue Jul 10 23:29:53 2007 +0200
+++ b/src/Pure/General/output.ML	Wed Jul 11 00:29:49 2007 +0200
@@ -31,6 +31,7 @@
   val output_width: string -> output * int
   val output: string -> output
   val escape: output -> string
+  val escape_malformed: string -> string
   val std_output: output -> unit
   val std_error: output -> unit
   val immediate_output: string -> unit
@@ -75,7 +76,9 @@
 
 fun output_width x = #output (get_mode ()) x;
 val output = #1 o output_width;
+
 fun escape x = #escape (get_mode ()) x;
+val escape_malformed = escape o translate_string output;