src/Pure/ML-Systems/smlnj.ML
changeset 10914 aded4ba99b88
parent 10725 ea048ad15283
child 12108 b6f10dcde803
     1.1 --- a/src/Pure/ML-Systems/smlnj.ML	Tue Jan 16 00:35:18 2001 +0100
     1.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Tue Jan 16 00:35:50 2001 +0100
     1.3 @@ -80,22 +80,21 @@
     1.4  
     1.5  (* ML command execution *)
     1.6  
     1.7 -fun use_text print verbose txt =
     1.8 +fun use_text (print, err) verbose txt =
     1.9    let
    1.10      val ref out_orig = Compiler.Control.Print.out;
    1.11  
    1.12      val out_buffer = ref ([]: string list);
    1.13      val out = {say = (fn s => out_buffer := s :: ! out_buffer), flush = (fn () => ())};
    1.14 -
    1.15 -    fun show_output () =
    1.16 +    fun output () =
    1.17        let val str = implode (rev (! out_buffer))
    1.18 -      in print (String.substring (str, 0, Int.max (0, size str - 1))) end;
    1.19 +      in String.substring (str, 0, Int.max (0, size str - 1)) end;
    1.20    in
    1.21      Compiler.Control.Print.out := out;
    1.22      Compiler.Interact.useStream (TextIO.openString txt) handle exn =>
    1.23 -      (Compiler.Control.Print.out := out_orig; show_output (); raise exn);
    1.24 +      (Compiler.Control.Print.out := out_orig; err (output ()); raise exn);
    1.25      Compiler.Control.Print.out := out_orig;
    1.26 -    if verbose then show_output () else ()
    1.27 +    if verbose then print (output ()) else ()
    1.28    end;
    1.29  
    1.30