# HG changeset patch
# User wenzelm
# Date 1481712825 -3600
# Node ID 5069ddebc9371963bba1f7342f28dfb227ea8b16
# Parent  fc66a76d6b9501c840731433fb99a7ce164243af
removed of_string_limited;

diff -r fc66a76d6b95 -r 5069ddebc937 src/Pure/General/source.ML
--- a/src/Pure/General/source.ML	Wed Dec 14 11:26:23 2016 +0100
+++ b/src/Pure/General/source.ML	Wed Dec 14 11:53:45 2016 +0100
@@ -14,9 +14,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_string: string -> (string, string list) source
   val exhausted: ('a, 'b) source -> ('a, 'a list) source
-  val of_string: string -> (string, string list) source
-  val of_string_limited: int -> string -> (string, substring) source
   val source': 'a -> 'b Scan.stopper -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
     ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source
   val source: 'a Scan.stopper -> ('a list -> 'b list * 'a list) ->
@@ -84,20 +83,9 @@
 
 fun of_list xs = make_source [] xs (fn xs => (xs, []));
 
-fun exhausted src = of_list (exhaust src);
-
-
-(* string source *)
-
 val of_string = of_list o raw_explode;
 
-fun of_string_limited limit str =
-  make_source [] (Substring.full str)
-    (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);
+fun exhausted src = of_list (exhaust src);