1.1 --- a/src/Pure/ML-Systems/polyml.ML Wed Oct 20 12:52:56 1999 +0200
1.2 +++ b/src/Pure/ML-Systems/polyml.ML Wed Oct 20 15:22:56 1999 +0200
1.3 @@ -49,6 +49,16 @@
1.4
1.5 (* ML command execution -- 'eval' *)
1.6
1.7 +local
1.8 +
1.9 +fun drop_last [] = []
1.10 + | drop_last [x] = []
1.11 + | drop_last (x :: xs) = x :: drop_last xs;
1.12 +
1.13 +val drop_last_char = implode o drop_last o explode;
1.14 +
1.15 +in
1.16 +
1.17 fun use_text print verbose txt =
1.18 let
1.19 val in_buffer = ref (explode txt);
1.20 @@ -65,7 +75,7 @@
1.21 [] => ()
1.22 | _ => (PolyML.compiler (get, put) (); exec ()));
1.23
1.24 - fun show_output () = print (implode (rev (! out_buffer)));
1.25 + fun show_output () = print (drop_last_char (implode (rev (! out_buffer))));
1.26 in
1.27 exec () handle exn => (show_output (); raise exn);
1.28 if verbose then show_output () else ()
1.29 @@ -83,17 +93,6 @@
1.30
1.31 (** OS related **)
1.32
1.33 -local
1.34 -
1.35 -fun drop_last [] = []
1.36 - | drop_last [x] = []
1.37 - | drop_last (x :: xs) = x :: drop_last xs;
1.38 -
1.39 -val drop_last_char = implode o drop_last o explode;
1.40 -
1.41 -in
1.42 -
1.43 -
1.44 (* system command execution *)
1.45
1.46 (*execute Unix command which doesn't take any input from stdin and
2.1 --- a/src/Pure/ML-Systems/smlnj.ML Wed Oct 20 12:52:56 1999 +0200
2.2 +++ b/src/Pure/ML-Systems/smlnj.ML Wed Oct 20 15:22:56 1999 +0200
2.3 @@ -87,7 +87,9 @@
2.4 val out_buffer = ref ([]: string list);
2.5 val out = {say = (fn s => out_buffer := s :: ! out_buffer), flush = (fn () => ())};
2.6
2.7 - fun show_output () = print (implode (rev (! out_buffer)));
2.8 + fun show_output () =
2.9 + let val str = implode (rev (! out_buffer))
2.10 + in print (String.substring (str, 0, Int.max (0, size str - 1))) end;
2.11 in
2.12 Compiler.Control.Print.out := out;
2.13 Compiler.Interact.useStream (TextIO.openString txt) handle exn =>