src/Pure/General/source.ML

   val get_single: ('a, 'b) source -> ('a * ('a, 'b) source) option
   val exhaust: ('a, 'b) source -> 'a list
   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 exhausted: ('a, 'b) source -> ('a, 'a list) source
   val of_string: string -> (string, string list) source
-  val exhausted: ('a, 'b) source -> ('a, 'a list) source
+  val of_string_limited: int -> string -> (string, substring) source
   val tty: (string, unit) source
   val source': 'a -> 'b Scan.stopper -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
     (bool * (string -> 'a * 'b list -> 'c list * ('a * 'b list))) option ->
     ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source
   val source: 'a Scan.stopper -> ('a list -> 'b list * 'a list) ->

 (** build sources **)
 
 (* list source *)
 
 fun of_list xs = make_source [] xs default_prompt (fn _ => fn xs => (xs, []));
-fun of_list_limited n xs = make_source [] xs default_prompt (fn _ => chop n);
+
+fun exhausted src = of_list (exhaust src);
+
+
+(* string source *)
 
 val of_string = of_list o explode;
 
-fun exhausted src = of_list (exhaust src);
+fun of_string_limited limit str =
+  make_source [] (Substring.full str) default_prompt
+    (fn _ => fn s =>
+      let
+        val (s1, s2) = Substring.splitAt (s, Int.min (Substring.size s, limit));
+        val cs = map String.str (Substring.explode s1);
+      in (cs, s2) end);
 
 
 (* stream source *)
 
 fun slurp_input instream =