16 val mapfilter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c) source) source |
16 val mapfilter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c) source) source |
17 val filter: ('a -> bool) -> ('a, 'b) source -> ('a, ('a, 'b) source) source |
17 val filter: ('a -> bool) -> ('a, 'b) source -> ('a, ('a, 'b) source) source |
18 val of_list: 'a list -> ('a, 'a list) source |
18 val of_list: 'a list -> ('a, 'a list) source |
19 val of_string: string -> (string, string list) source |
19 val of_string: string -> (string, string list) source |
20 val of_file: string -> (string, string list) source |
20 val of_file: string -> (string, string list) source |
|
21 val wakeup: string ref |
21 val of_stream: TextIO.instream -> TextIO.outstream -> (string, unit) source |
22 val of_stream: TextIO.instream -> TextIO.outstream -> (string, unit) source |
22 val tty: (string, unit) source |
23 val tty: (string, unit) source |
23 val source': 'a -> 'b * ('b -> bool) -> ('a * 'b list -> 'c list * ('a * 'b list)) -> |
24 val source': 'a -> 'b * ('b -> bool) -> ('a * 'b list -> 'c list * ('a * 'b list)) -> |
24 ('a * 'b list -> 'd * ('a * 'b list)) option -> |
25 ('a * 'b list -> 'd * ('a * 'b list)) option -> |
25 ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source |
26 ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source |
110 val of_file = of_string o File.read; |
111 val of_file = of_string o File.read; |
111 |
112 |
112 |
113 |
113 (* stream source *) |
114 (* stream source *) |
114 |
115 |
|
116 val wakeup = ref ""; |
|
117 |
115 fun drain_stream instream outstream prompt () = |
118 fun drain_stream instream outstream prompt () = |
116 (TextIO.output (outstream, prompt); |
119 (TextIO.output (outstream, ! wakeup ^ prompt); |
117 TextIO.flushOut outstream; |
120 TextIO.flushOut outstream; |
118 (explode (TextIO.inputLine instream), ())); |
121 (explode (TextIO.inputLine instream), ())); |
119 |
122 |
120 fun of_stream instream outstream = |
123 fun of_stream instream outstream = |
121 make_source [] () default_prompt (drain_stream instream outstream); |
124 make_source [] () default_prompt (drain_stream instream outstream); |