# HG changeset patch
# User wenzelm
# Date 1184881744 -7200
# Node ID e22705ccc07d04e47c60241e752e83e90247169f
# Parent  4642a2eefe74051f329a2ed343e5099dde59e4e0
added of_string_limited (more efficient for partial scans);

diff -r 4642a2eefe74 -r e22705ccc07d src/Pure/General/source.ML
--- 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);