--- a/src/Pure/General/source.ML Thu Jul 19 23:49:02 2007 +0200
+++ b/src/Pure/General/source.ML Thu Jul 19 23:49:04 2007 +0200
@@ -18,6 +18,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 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
@@ -104,6 +105,10 @@
fun of_list xs = make_source [] xs default_prompt (fn _ => fn xs => (xs, []));
val of_string = of_list o explode;
+fun of_string_limited s =
+ let val cs = explode s
+ in make_source [] cs default_prompt (fn _ => chop 8000) end;
+
fun exhausted src = of_list (exhaust src);