equal
deleted
inserted
replaced
36 if String.isPrefix bef s then |
36 if String.isPrefix bef s then |
37 aux seen "" ^ aft ^ aux [] (unprefix bef s) |
37 aux seen "" ^ aft ^ aux [] (unprefix bef s) |
38 else |
38 else |
39 aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE)) |
39 aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE)) |
40 in aux [] end |
40 in aux [] end |
41 |
|
42 fun remove_all bef = replace_all bef "" |
41 fun remove_all bef = replace_all bef "" |
43 |
42 |
44 val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now |
43 val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now |
45 |
44 |
46 fun parse_bool_option option name s = |
45 fun parse_bool_option option name s = |