--- 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;