equal
deleted
inserted
replaced
231 val scan_nat = repeat1 (one Symbol.is_digit) >> nat_of_list |
231 val scan_nat = repeat1 (one Symbol.is_digit) >> nat_of_list |
232 |
232 |
233 fun this [] = (fn toks => ([], toks)) |
233 fun this [] = (fn toks => ([], toks)) |
234 | this (xs' as (x::xs)) = one (fn y => x=y) -- this xs >> K xs' |
234 | this (xs' as (x::xs)) = one (fn y => x=y) -- this xs >> K xs' |
235 |
235 |
236 fun this_string s = this (explode s) >> K s |
236 fun this_string s = this (raw_explode s) >> K s |
237 |
237 |
238 end |
238 end |