# HG changeset patch
# User wenzelm
# Date 1185741715 -7200
# Node ID 7be344a20b6bdcfb7eec89fe73ccac526ef949ce
# Parent  736c03ae92f56120706712b763e2fd97221e090f
added of_list_limited (with limit argument);
removed of_string_limited;

diff -r 736c03ae92f5 -r 7be344a20b6b src/Pure/General/source.ML
--- a/src/Pure/General/source.ML	Sun Jul 29 19:46:04 2007 +0200
+++ b/src/Pure/General/source.ML	Sun Jul 29 22:41:55 2007 +0200
@@ -17,8 +17,8 @@
   val map_filter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c) source) source
   val filter: ('a -> bool) -> ('a, 'b) source -> ('a, ('a, 'b) source) source
   val of_list: 'a list -> ('a, 'a list) source
+  val of_list_limited: int -> 'a list -> ('a, 'a list) source
   val of_string: string -> (string, string list) source
-  val of_string_limited: 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
@@ -103,11 +103,9 @@
 (* list source *)
 
 fun of_list xs = make_source [] xs default_prompt (fn _ => fn xs => (xs, []));
-val of_string = of_list o explode;
+fun of_list_limited n xs = make_source [] xs default_prompt (fn _ => chop n);
 
-fun of_string_limited s =
-  let val cs = explode s
-  in make_source [] cs default_prompt (fn _ => chop 8000) end;
+val of_string = of_list o explode;
 
 fun exhausted src = of_list (exhaust src);