use_ml: reverted to simple output (Poly/ML changed);
authorwenzelm
Fri Dec 29 03:57:01 2006 +0100 (2006-12-29)
changeset 21923663108ee4eef
parent 21922 76e1fce071aa
child 21924 fe474e69e603
use_ml: reverted to simple output (Poly/ML changed);
src/Pure/ML-Systems/polyml-5.0.ML
     1.1 --- a/src/Pure/ML-Systems/polyml-5.0.ML	Thu Dec 28 16:49:35 2006 +0100
     1.2 +++ b/src/Pure/ML-Systems/polyml-5.0.ML	Fri Dec 29 03:57:01 2006 +0100
     1.3 @@ -14,8 +14,6 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun std_output s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
     1.8 -
     1.9  fun use_ml name (print, err) verbose txt =
    1.10    let
    1.11      val in_buffer = ref (explode txt);
    1.12 @@ -28,16 +26,15 @@
    1.13        (case ! in_buffer of
    1.14          [] => ""
    1.15        | c :: cs => (in_buffer := cs; if c = "\n" then line_no := ! line_no + 1 else (); c));
    1.16 -    val put_fn = ref (fn s => out_buffer := s :: ! out_buffer);
    1.17 +    fun put s = out_buffer := s :: ! out_buffer;
    1.18  
    1.19      fun exec () =
    1.20        (case ! in_buffer of
    1.21          [] => ()
    1.22 -      | _ => (PolyML.compilerEx (get, fn s => ! put_fn s, line, name) (); exec ()));
    1.23 +      | _ => (PolyML.compilerEx (get, put, line, name) (); exec ()));
    1.24    in
    1.25      exec () handle exn => (err (output ()); raise exn);
    1.26 -    if verbose then print (output ()) else ();
    1.27 -    put_fn := std_output   (*run-time output, e.g. PolyML.print*)
    1.28 +    if verbose then print (output ()) else ()
    1.29    end;
    1.30  
    1.31  in