let trim str =
let start_non_blank = ref 0 in
let stop_non_blank = ref ((String.length str) - 1) in
while !start_non_blank < String.length str &&
is_whitespace (str.[!start_non_blank]) do
incr start_non_blank
done;
while !start_non_blank <= !stop_non_blank &&
is_whitespace (str.[!stop_non_blank]) do
decr stop_non_blank
done;
String.sub str !start_non_blank (!stop_non_blank - !start_non_blank + 1)