# HG changeset patch
# User wenzelm
# Date 1167361021 -3600
# Node ID 663108ee4eef4a26b6dd9447697ebeaa41a127b5
# Parent  76e1fce071aae730e8d85316e10d9bfb4392cb98
use_ml: reverted to simple output (Poly/ML changed);

diff -r 76e1fce071aa -r 663108ee4eef src/Pure/ML-Systems/polyml-5.0.ML
--- a/src/Pure/ML-Systems/polyml-5.0.ML	Thu Dec 28 16:49:35 2006 +0100
+++ b/src/Pure/ML-Systems/polyml-5.0.ML	Fri Dec 29 03:57:01 2006 +0100
@@ -14,8 +14,6 @@
 
 local
 
-fun std_output s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
-
 fun use_ml name (print, err) verbose txt =
   let
     val in_buffer = ref (explode txt);
@@ -28,16 +26,15 @@
       (case ! in_buffer of
         [] => ""
       | c :: cs => (in_buffer := cs; if c = "\n" then line_no := ! line_no + 1 else (); c));
-    val put_fn = ref (fn s => out_buffer := s :: ! out_buffer);
+    fun put s = out_buffer := s :: ! out_buffer;
 
     fun exec () =
       (case ! in_buffer of
         [] => ()
-      | _ => (PolyML.compilerEx (get, fn s => ! put_fn s, line, name) (); exec ()));
+      | _ => (PolyML.compilerEx (get, put, line, name) (); exec ()));
   in
     exec () handle exn => (err (output ()); raise exn);
-    if verbose then print (output ()) else ();
-    put_fn := std_output   (*run-time output, e.g. PolyML.print*)
+    if verbose then print (output ()) else ()
   end;
 
 in