# HG changeset patch
# User wenzelm
# Date 1191270598 -7200
# Node ID 7c9a970d7ab52df752fe43624073e822d6c11e35
# Parent  f66ab1dfbae1ca6ebc77b58ae30b7012007953b1
fixed use_text;

diff -r f66ab1dfbae1 -r 7c9a970d7ab5 src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Mon Oct 01 22:29:56 2007 +0200
+++ b/src/Pure/ML-Systems/mosml.ML	Mon Oct 01 22:29:58 2007 +0200
@@ -15,6 +15,9 @@
 > Session.finish ();
 > cd "../FOL";
 > use "ROOT.ML";
+> Session.finish ();
+> cd "../ZF";
+> use "ROOT.ML";
 *)
 
 (** ML system related **)
@@ -43,6 +46,7 @@
 (*proper implementation available?*)
 structure IntInf =
 struct
+  fun divMod (x, y) = (x div y, x mod y);
   open Int;
 end;
 
@@ -145,18 +149,18 @@
 (* ML command execution *)
 
 (*Can one redirect 'use' directly to an instream?*)
-fun use_text _ _ _ txt =
+fun use_text (tune: string -> string) _ _ _ txt =
   let
     val tmp_name = FileSys.tmpName ();
     val tmp_file = TextIO.openOut tmp_name;
   in
-    TextIO.output (tmp_file, txt);
+    TextIO.output (tmp_file, tune txt);
     TextIO.closeOut tmp_file;
     use tmp_name;
     FileSys.remove tmp_name
   end;
 
-fun use_file _ _ name = use name;
+fun use_file _ _ _ name = use name;