12 val get_single: ('a, 'b) source -> ('a * ('a, 'b) source) option |
12 val get_single: ('a, 'b) source -> ('a * ('a, 'b) source) option |
13 val exhaust: ('a, 'b) source -> 'a list |
13 val exhaust: ('a, 'b) source -> 'a list |
14 val map_filter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c) source) source |
14 val map_filter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c) source) source |
15 val filter: ('a -> bool) -> ('a, 'b) source -> ('a, ('a, 'b) source) source |
15 val filter: ('a -> bool) -> ('a, 'b) source -> ('a, ('a, 'b) source) source |
16 val of_list: 'a list -> ('a, 'a list) source |
16 val of_list: 'a list -> ('a, 'a list) source |
|
17 val of_string: string -> (string, string list) source |
17 val exhausted: ('a, 'b) source -> ('a, 'a list) source |
18 val exhausted: ('a, 'b) source -> ('a, 'a list) source |
18 val of_string: string -> (string, string list) source |
|
19 val of_string_limited: int -> string -> (string, substring) source |
|
20 val source': 'a -> 'b Scan.stopper -> ('a * 'b list -> 'c list * ('a * 'b list)) -> |
19 val source': 'a -> 'b Scan.stopper -> ('a * 'b list -> 'c list * ('a * 'b list)) -> |
21 ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source |
20 ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source |
22 val source: 'a Scan.stopper -> ('a list -> 'b list * 'a list) -> |
21 val source: 'a Scan.stopper -> ('a list -> 'b list * 'a list) -> |
23 ('a, 'd) source -> ('b, ('a, 'd) source) source |
22 ('a, 'd) source -> ('b, ('a, 'd) source) source |
24 end; |
23 end; |
82 |
81 |
83 (* list source *) |
82 (* list source *) |
84 |
83 |
85 fun of_list xs = make_source [] xs (fn xs => (xs, [])); |
84 fun of_list xs = make_source [] xs (fn xs => (xs, [])); |
86 |
85 |
87 fun exhausted src = of_list (exhaust src); |
|
88 |
|
89 |
|
90 (* string source *) |
|
91 |
|
92 val of_string = of_list o raw_explode; |
86 val of_string = of_list o raw_explode; |
93 |
87 |
94 fun of_string_limited limit str = |
88 fun exhausted src = of_list (exhaust src); |
95 make_source [] (Substring.full str) |
|
96 (fn s => |
|
97 let |
|
98 val (s1, s2) = Substring.splitAt (s, Int.min (Substring.size s, limit)); |
|
99 val cs = map String.str (Substring.explode s1); |
|
100 in (cs, s2) end); |
|
101 |
89 |
102 |
90 |
103 |
91 |
104 (** cascade sources **) |
92 (** cascade sources **) |
105 |
93 |