# HG changeset patch
# User wenzelm
# Date 1283001932 -7200
# Node ID be9dace0ff58742a57a29b67bc728d9fa8cbe1bc
# Parent  62f6ba39b3d45aab3c22298083275b6a7e55c5d5
non-critical output primitives -- depending on thread-safe TextIO, while races wrt. flushing should not matter;

diff -r 62f6ba39b3d4 -r be9dace0ff58 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Fri Aug 27 22:30:25 2010 +0200
+++ b/src/Pure/General/output.ML	Sat Aug 28 15:25:32 2010 +0200
@@ -79,11 +79,8 @@
 
 (* output primitives -- normally NOT used directly!*)
 
-fun std_output s = NAMED_CRITICAL "IO" (fn () =>
-  (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut));
-
-fun std_error s = NAMED_CRITICAL "IO" (fn () =>
-  (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr));
+fun std_output s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
+fun std_error s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
 
 fun writeln_default "" = ()
   | writeln_default s = std_output (suffix "\n" s);