# HG changeset patch
# User wenzelm
# Date 1166129219 -3600
# Node ID ae37078923102d0ae14c547fb73cc44b323fdc38
# Parent  7f2853bd54bfefad9a946e3df183e15f0fc0a84c
activated improved use_ml, which captures output and reports source positions;
define use_file in terms of use_ml;

diff -r 7f2853bd54bf -r ae3707892310 src/Pure/ML-Systems/polyml-5.0.ML
--- a/src/Pure/ML-Systems/polyml-5.0.ML	Thu Dec 14 21:46:58 2006 +0100
+++ b/src/Pure/ML-Systems/polyml-5.0.ML	Thu Dec 14 21:46:59 2006 +0100
@@ -11,9 +11,11 @@
 
 
 (* improved versions of use_text/file *)
-(*
+
 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);
@@ -26,15 +28,16 @@
       (case ! in_buffer of
         [] => ""
       | c :: cs => (in_buffer := cs; if c = "\n" then line_no := ! line_no + 1 else (); c));
-    fun put s = out_buffer := s :: ! out_buffer;
+    val put_fn = ref (fn s => out_buffer := s :: ! out_buffer);
 
     fun exec () =
       (case ! in_buffer of
         [] => ()
-      | _ => (PolyML.compilerEx (get, put, line, name) (); exec ()));
+      | _ => (PolyML.compilerEx (get, fn s => ! put_fn s, line, name) (); exec ()));
   in
     exec () handle exn => (err (output ()); raise exn);
-    if verbose then print (output ()) else ()
+    if verbose then print (output ()) else ();
+    put_fn := std_output   (*run-time output, e.g. PolyML.print*)
   end;
 
 in
@@ -48,4 +51,3 @@
   in use_ml name output verbose txt end;
 
 end;
-*)