use_text: remove last char from output;
authorwenzelm
Wed, 20 Oct 1999 15:22:56 +0200
changeset 7890 0aa16bc2abdb
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
--- a/src/Pure/ML-Systems/polyml.ML	Wed Oct 20 12:52:56 1999 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Wed Oct 20 15:22:56 1999 +0200
@@ -49,6 +49,16 @@
 
 (* ML command execution -- 'eval' *)
 
+local
+
+fun drop_last [] = []
+  | drop_last [x] = []
+  | drop_last (x :: xs) = x :: drop_last xs;
+
+val drop_last_char = implode o drop_last o explode;
+
+in
+
 fun use_text print verbose txt =
   let
     val in_buffer = ref (explode txt);
@@ -65,7 +75,7 @@
         [] => ()
       | _ => (PolyML.compiler (get, put) (); exec ()));
 
-    fun show_output () = print (implode (rev (! out_buffer)));
+    fun show_output () = print (drop_last_char (implode (rev (! out_buffer))));
   in
     exec () handle exn => (show_output (); raise exn);
     if verbose then show_output () else ()
@@ -83,17 +93,6 @@
 
 (** OS related **)
 
-local
-
-fun drop_last [] = []
-  | drop_last [x] = []
-  | drop_last (x :: xs) = x :: drop_last xs;
-
-val drop_last_char = implode o drop_last o explode;
-
-in
-
-
 (* system command execution *)
 
 (*execute Unix command which doesn't take any input from stdin and
--- a/src/Pure/ML-Systems/smlnj.ML	Wed Oct 20 12:52:56 1999 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Wed Oct 20 15:22:56 1999 +0200
@@ -87,7 +87,9 @@
     val out_buffer = ref ([]: string list);
     val out = {say = (fn s => out_buffer := s :: ! out_buffer), flush = (fn () => ())};
 
-    fun show_output () = print (implode (rev (! out_buffer)));
+    fun show_output () =
+      let val str = implode (rev (! out_buffer))
+      in print (String.substring (str, 0, Int.max (0, size str - 1))) end;
   in
     Compiler.Control.Print.out := out;
     Compiler.Interact.useStream (TextIO.openString txt) handle exn =>