removed of_string_limited;
authorwenzelm
Wed Dec 14 11:53:45 2016 +0100 (2016-12-14)
changeset 645655069ddebc937
parent 64564 fc66a76d6b95
child 64566 679710d324f1
removed of_string_limited;
src/Pure/General/source.ML
     1.1 --- a/src/Pure/General/source.ML	Wed Dec 14 11:26:23 2016 +0100
     1.2 +++ b/src/Pure/General/source.ML	Wed Dec 14 11:53:45 2016 +0100
     1.3 @@ -14,9 +14,8 @@
     1.4    val map_filter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c) source) source
     1.5    val filter: ('a -> bool) -> ('a, 'b) source -> ('a, ('a, 'b) source) source
     1.6    val of_list: 'a list -> ('a, 'a list) source
     1.7 +  val of_string: string -> (string, string list) source
     1.8    val exhausted: ('a, 'b) source -> ('a, 'a list) source
     1.9 -  val of_string: string -> (string, string list) source
    1.10 -  val of_string_limited: int -> string -> (string, substring) source
    1.11    val source': 'a -> 'b Scan.stopper -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
    1.12      ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source
    1.13    val source: 'a Scan.stopper -> ('a list -> 'b list * 'a list) ->
    1.14 @@ -84,20 +83,9 @@
    1.15  
    1.16  fun of_list xs = make_source [] xs (fn xs => (xs, []));
    1.17  
    1.18 -fun exhausted src = of_list (exhaust src);
    1.19 -
    1.20 -
    1.21 -(* string source *)
    1.22 -
    1.23  val of_string = of_list o raw_explode;
    1.24  
    1.25 -fun of_string_limited limit str =
    1.26 -  make_source [] (Substring.full str)
    1.27 -    (fn s =>
    1.28 -      let
    1.29 -        val (s1, s2) = Substring.splitAt (s, Int.min (Substring.size s, limit));
    1.30 -        val cs = map String.str (Substring.explode s1);
    1.31 -      in (cs, s2) end);
    1.32 +fun exhausted src = of_list (exhaust src);
    1.33  
    1.34  
    1.35