use_text: remove last char from output;
authorwenzelm
Wed, 20 Oct 1999 15:22:56 +0200
changeset 78900aa16bc2abdb
parent 7889 56e91ac0f074
child 7891 c77ad0c3c92f
use_text: remove last char from output;
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/smlnj.ML
     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 =>