skip_whitespace() shouldn't claim its return value is const, it doesn't know