equal
deleted
inserted
replaced
157 in Exn.release res end); |
157 in Exn.release res end); |
158 |
158 |
159 |
159 |
160 (* digesting *) |
160 (* digesting *) |
161 |
161 |
162 fun hex_digit i = if i < 10 then chr (Char.ord #"0" + i) else chr (Char.ord #"a" + i - 10); |
|
163 fun hex_string byte = op ^ (apply2 hex_digit (Integer.div_mod (Word8.toInt byte) 16)); |
162 fun hex_string byte = op ^ (apply2 hex_digit (Integer.div_mod (Word8.toInt byte) 16)); |
164 |
163 |
165 in |
164 in |
166 |
165 |
167 fun digest_string_external str = |
166 fun digest_string_external str = |