# HG changeset patch
# User wenzelm
# Date 1114537937 -7200
# Node ID 6b445e021bc8f441e0b1bd4f332cc812cf66d0c6
# Parent  30e878979457aba9f6631895973ea37b4ab8f593
eval command line: show results;
tuned;

diff -r 30e878979457 -r 6b445e021bc8 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Tue Apr 26 19:51:56 2005 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Tue Apr 26 19:52:17 2005 +0200
@@ -87,7 +87,7 @@
 local
   fun println s =
     (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut);
-  val eval = use_text (println, println) false;
+  val eval = use_text (println, println) true;
 in
   val _ = PolyML.onEntry (fn () => app eval (CommandLine.arguments ()));
 end;
@@ -165,7 +165,7 @@
   | SOME txt => txt);
 
 
-(* profiling: version that works even with 
+(* profiling: version that works even with
 ML{*profiling 1*}
 apply \\<dots>
 ML{*profiling 0*}
@@ -183,18 +183,16 @@
   structure IO =
   struct
   open OriginalIO
-  val mkTextReader = mkReader 
-  val mkTextWriter = mkWriter 
+  val mkTextReader = mkReader
+  val mkTextWriter = mkWriter
   end;
 end;
 
-(** This extension of the Poly/ML Signal structure is only necessary
-    because in SML/NJ, types Posix.Signal.signal and Signals.signal differ.**)
-
+(*This extension of the Poly/ML Signal structure is only necessary
+  because in SML/NJ, types Posix.Signal.signal and Signals.signal differ.*)
 structure IsaSignal =
 struct
-open Signal
-val usr1 = Posix.Signal.usr1 
-val usr2 = Posix.Signal.usr2 
+  open Signal
+  val usr1 = Posix.Signal.usr1
+  val usr2 = Posix.Signal.usr2
 end;
-