eliminated Output.ml_output;
authorwenzelm
Mon, 23 Mar 2009 22:38:02 +0100
changeset 30677 df6ca2f50199
parent 30676 edca392a2abb
child 30678 35d40d961ed2
eliminated Output.ml_output;
src/Pure/ML/ml_test.ML
--- a/src/Pure/ML/ml_test.ML	Mon Mar 23 22:37:41 2009 +0100
+++ b/src/Pure/ML/ml_test.ML	Mon Mar 23 22:38:02 2009 +0100
@@ -27,8 +27,6 @@
 
 fun eval do_run verbose pos toks =
   let
-    val (print, err) = Output.ml_output;
-
     val input = toks |> map (fn tok =>
       (serial (), (String.explode (ML_Lex.text_of tok), ML_Lex.pos_of tok)));
     val index_pos = Inttab.lookup (Inttab.make (map (apsnd snd) input));
@@ -78,8 +76,8 @@
         PolyML.compiler (get, parameters) ())
       handle exn =>
        (put ("Exception- " ^ General.exnMessage exn ^ " raised");
-        err (output ()); raise exn);
-  in if verbose then print (output ()) else () end;
+        error (output ()); raise exn);
+  in if verbose then writeln (output ()) else () end;
 
 
 (* ML test command *)