# HG changeset patch # User wenzelm # Date 961969612 -7200 # Node ID f8f54877a18c6d3b61ce181ca360897ccd037ca3 # Parent addbea3446738dc2bd47646a65dfb8805b56cc5e added exhausted: ('a, 'b) source -> ('a, 'a list) source; diff -r addbea344673 -r f8f54877a18c src/Pure/General/source.ML --- a/src/Pure/General/source.ML Sun Jun 25 23:46:39 2000 +0200 +++ b/src/Pure/General/source.ML Sun Jun 25 23:46:52 2000 +0200 @@ -19,6 +19,7 @@ val filter: ('a -> bool) -> ('a, 'b) source -> ('a, ('a, 'b) source) source val of_list: 'a list -> ('a, 'a list) source 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 tty: (string, unit) source val source': 'a -> 'b * ('b -> bool) -> ('a * 'b list -> 'c list * ('a * 'b list)) -> @@ -109,6 +110,8 @@ fun of_list xs = make_source [] xs default_prompt drain_list; val of_string = of_list o explode; +fun exhausted src = of_list (exhaust src); + (* stream source *)