Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use_output: proper handling of non-ASCII symbols;
authorwenzelm
Tue, 16 Jan 2001 21:54:43 +0100
changeset 10924 92305ae9f460
parent 10923 e34948f18541
child 10925 5ffe7ed8899a
use_output: proper handling of non-ASCII symbols;
src/Pure/context.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle