--- a/src/Pure/General/source.ML Wed Sep 27 21:32:15 2006 +0200
+++ b/src/Pure/General/source.ML Wed Sep 27 21:33:13 2006 +0200
@@ -20,7 +20,6 @@
val of_string: string -> (string, string list) source
val exhausted: ('a, 'b) source -> ('a, 'a list) source
val of_stream: TextIO.instream -> TextIO.outstream -> (string, unit) source
- val of_instream_slurp: TextIO.instream -> (string, unit) source
val tty: (string, unit) source
val source': 'a -> 'b * ('b -> bool) -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
('a * 'b list -> 'c list * ('a * 'b list)) option ->
@@ -134,21 +133,6 @@
val tty = of_stream TextIO.stdIn TextIO.stdOut;
-(* no prompt output, slurp input eagerly *)
-(* NB: if canInput isn't supported, falls back to line input *)
-
-fun drain_stream' instream _ () =
- let fun lines xs =
- (case TextIO.canInput (instream, 1) of
- NONE => xs
- | SOME 0 => ""::xs (* EOF *)
- | SOME _ => lines ((TextIO.inputLine instream) :: xs))
- handle Io => xs
- in (flat (map explode (rev (lines [TextIO.inputLine instream]))), ()) end;
-
-fun of_instream_slurp instream =
- make_source [] () default_prompt (drain_stream' instream);
-
(** compose sources **)