stream source: non-critical, assuming exclusive ownership;
authorwenzelm
Sun Aug 12 18:53:04 2007 +0200 (2007-08-12)
changeset 24232a70360a54e5c
parent 24231 85fb973a8207
child 24233 5bec1b4149e7
stream source: non-critical, assuming exclusive ownership;
src/Pure/General/source.ML
     1.1 --- a/src/Pure/General/source.ML	Sun Aug 12 18:53:03 2007 +0200
     1.2 +++ b/src/Pure/General/source.ML	Sun Aug 12 18:53:04 2007 +0200
     1.3 @@ -112,24 +112,23 @@
     1.4  
     1.5  (* stream source *)
     1.6  
     1.7 -fun slurp_input instream = NAMED_CRITICAL "IO" (fn () =>
     1.8 +fun slurp_input instream =
     1.9    let
    1.10      fun slurp () =
    1.11        (case TextIO.canInput (instream, 1) handle IO.Io _ => NONE of
    1.12          NONE => []
    1.13        | SOME 0 => []
    1.14        | SOME _ => TextIO.input instream :: slurp ());
    1.15 -  in maps explode (slurp ()) end);
    1.16 +  in maps explode (slurp ()) end;
    1.17  
    1.18  fun drain_stream instream outstream prompt () =
    1.19    let val input = slurp_input instream in
    1.20      if exists (fn c => c = "\n") input then (input, ())
    1.21      else
    1.22        (case
    1.23 -        NAMED_CRITICAL "IO" (fn () =>
    1.24            (TextIO.output (outstream, Output.output prompt);
    1.25              TextIO.flushOut outstream;
    1.26 -            TextIO.inputLine instream)) of
    1.27 +            TextIO.inputLine instream) of
    1.28            SOME line => (input @ explode line, ())
    1.29          | NONE => (input, ()))
    1.30    end;