# HG changeset patch
# User wenzelm
# Date 1186937584 -7200
# Node ID a70360a54e5c59e8d059708e4b1032e909df04b5
# Parent  85fb973a8207e5873e421add195de50c686f1990
stream source: non-critical, assuming exclusive ownership;

diff -r 85fb973a8207 -r a70360a54e5c src/Pure/General/source.ML
--- a/src/Pure/General/source.ML	Sun Aug 12 18:53:03 2007 +0200
+++ b/src/Pure/General/source.ML	Sun Aug 12 18:53:04 2007 +0200
@@ -112,24 +112,23 @@
 
 (* stream source *)
 
-fun slurp_input instream = NAMED_CRITICAL "IO" (fn () =>
+fun slurp_input instream =
   let
     fun slurp () =
       (case TextIO.canInput (instream, 1) handle IO.Io _ => NONE of
         NONE => []
       | SOME 0 => []
       | SOME _ => TextIO.input instream :: slurp ());
-  in maps explode (slurp ()) end);
+  in maps explode (slurp ()) end;
 
 fun drain_stream instream outstream prompt () =
   let val input = slurp_input instream in
     if exists (fn c => c = "\n") input then (input, ())
     else
       (case
-        NAMED_CRITICAL "IO" (fn () =>
           (TextIO.output (outstream, Output.output prompt);
             TextIO.flushOut outstream;
-            TextIO.inputLine instream)) of
+            TextIO.inputLine instream) of
           SOME line => (input @ explode line, ())
         | NONE => (input, ()))
   end;