# HG changeset patch # User wenzelm # Date 940425776 -7200 # Node ID 0aa16bc2abdb1b58aaa3e6e99dc608b217b79d3c # Parent 56e91ac0f07489a115ec401da239993d1e74c932 use_text: remove last char from output; diff -r 56e91ac0f074 -r 0aa16bc2abdb src/Pure/ML-Systems/polyml.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 diff -r 56e91ac0f074 -r 0aa16bc2abdb src/Pure/ML-Systems/smlnj.ML --- 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 =>