# HG changeset patch
# User wenzelm
# Date 979678483 -3600
# Node ID 92305ae9f460b9e5963bd7aee89430910159ec0a
# Parent  e34948f185419b90a31cc7552a2f083d4812c1ab
use_output: proper handling of non-ASCII symbols;

diff -r e34948f18541 -r 92305ae9f460 src/Pure/context.ML
--- a/src/Pure/context.ML	Tue Jan 16 21:53:57 2001 +0100
+++ b/src/Pure/context.ML	Tue Jan 16 21:54:43 2001 +0100
@@ -71,9 +71,10 @@
 (* use ML text *)
 
 val ml_output = (writeln, error_msg: string -> unit);
+fun use_output verb txt = use_text ml_output verb (Symbol.plain_output txt);
 
-fun use_mltext txt verb opt_thy = setmp opt_thy (fn () => use_text ml_output verb txt) ();
-fun use_mltext_theory txt verb thy = #2 (pass_theory thy (use_text ml_output verb) txt);
+fun use_mltext txt verb opt_thy = setmp opt_thy (fn () => use_output verb txt) ();
+fun use_mltext_theory txt verb thy = #2 (pass_theory thy (use_output verb) txt);
 
 fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");") false;