Source.of_list: no buffer limitation (now pointless due to tail-recursive Scan.repeat);

--- a/src/Pure/General/source.ML	Mon May 10 19:25:59 2004 +0200
+++ b/src/Pure/General/source.ML	Mon May 10 19:26:11 2004 +0200
@@ -102,12 +102,7 @@
 
 (* list source *)
 
-(*limiting the input buffer considerably improves performance*)
-val limit = 4000;
-
-fun drain_list _ xs = (take (limit, xs), drop (limit, xs));
-
-fun of_list xs = make_source [] xs default_prompt drain_list;
+fun of_list xs = make_source [] xs default_prompt (fn _ => fn xs => (xs, []));
 val of_string = of_list o explode;
 
 fun exhausted src = of_list (exhaust src);