# HG changeset patch
# User wenzelm
# Date 1197045605 -3600
# Node ID fee953b4501554b31557c9a6348b92b02c0f7ff0
# Parent  016f677ad7b8a737ad8376faed9ae85faa1e1508
output_prompt: CRITICAL;

diff -r 016f677ad7b8 -r fee953b45015 src/Pure/General/source.ML
--- a/src/Pure/General/source.ML	Fri Dec 07 15:08:09 2007 +0100
+++ b/src/Pure/General/source.ML	Fri Dec 07 17:40:05 2007 +0100
@@ -122,15 +122,16 @@
   in maps explode (slurp ()) end;
 
 fun drain_stream instream outstream prompt () =
-  let val input = slurp_input instream in
+  let
+    val input = slurp_input instream;
+    fun output_prompt () = NAMED_CRITICAL "IO" (fn () =>
+      (TextIO.output (outstream, Output.output prompt); TextIO.flushOut outstream));
+  in
     if exists (fn c => c = "\n") input then (input, ())
     else
-      (case
-          (TextIO.output (outstream, Output.output prompt);
-            TextIO.flushOut outstream;
-            TextIO.inputLine instream) of
-          SOME line => (input @ explode line, ())
-        | NONE => (input, ()))
+      (case (output_prompt (); TextIO.inputLine instream) of
+        SOME line => (input @ explode line, ())
+      | NONE => (input, ()))
   end;
 
 fun of_stream instream outstream =