# HG changeset patch
# User wenzelm
# Date 1184106589 -7200
# Node ID 39f8d1480d55886f00af544a663e2e464c6a6555
# Parent  2ebecff57b178a32f054020123bb0d6a7968c641
added escape_malformed (failsafe);

diff -r 2ebecff57b17 -r 39f8d1480d55 src/Pure/General/output.ML
--- 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;