Use our own isspace() function since the standard-library isspace()
sometimes gives incorrect results for non-ASCII characters.