// Skips whitespace and then reads a non-whitespace string.
// If stream.width() is greater than 0, at most stream.width()-1 non-whitespace
// characters are read. When done, stream.width(0) is called.
// If EOF is encountered, the stream's eofbit is set.
// Skips whitespace and then reads a non-whitespace string.
// If stream.width() is greater than 0, at most stream.width()-1 non-whitespace
// characters are read. When done, stream.width(0) is called.
// If EOF is encountered, the stream's eofbit is set.