# HG changeset patch
# User wenzelm
# Date 1114278671 -7200
# Node ID df958c7afe5049b196b940c0232e6c088adf6148
# Parent  aa58e4ec3a1fb8c4136356e645f034caf3105ca6
eval command line arguments;
tuned;

diff -r aa58e4ec3a1f -r df958c7afe50 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Sat Apr 23 19:51:04 2005 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Sat Apr 23 19:51:11 2005 +0200
@@ -57,15 +57,13 @@
   | 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, err) verbose txt =
   let
     val in_buffer = ref (explode txt);
     val out_buffer = ref ([]: string list);
-    fun output () = drop_last_char (implode (rev (! out_buffer)));
+    fun output () = implode (drop_last (rev (! out_buffer)));
 
     fun get () =
       (case ! in_buffer of
@@ -85,6 +83,16 @@
 end;
 
 
+(*eval command line arguments*)
+local
+  fun println s =
+    (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut);
+  val eval = use_text (println, println) false;
+in
+  val _ = PolyML.onEntry (fn () => app eval (CommandLine.arguments ()));
+end;
+
+
 
 (** interrupts **)