equal
deleted
inserted
replaced
58 if Substring.first post = SOME #"+" |
58 if Substring.first post = SOME #"+" |
59 (* Substring.isPrefix "+" post *)(* seg fault in Poly/ML 5.1 *) |
59 (* Substring.isPrefix "+" post *)(* seg fault in Poly/ML 5.1 *) |
60 then f (Substring.full " "::pre::done, Substring.triml 1 post) |
60 then f (Substring.full " "::pre::done, Substring.triml 1 post) |
61 else let |
61 else let |
62 val (c, rest) = Substring.splitAt (post, 3) |
62 val (c, rest) = Substring.splitAt (post, 3) |
63 handle Subscript => |
63 handle General.Subscript => |
64 (Substring.full "%25", Substring.triml 1 post); |
64 (Substring.full "%25", Substring.triml 1 post); |
65 in f (to_char c::pre::done, rest) end |
65 in f (to_char c::pre::done, rest) end |
66 end; |
66 end; |
67 in f ([], s) end; |
67 in f ([], s) end; |
68 |
68 |