def read_next_token(s, pos):
   """This function, given a string s (probably a long string, like a line or a file)
      and a position 'pos', finds the next token in the string (defined as a nonempty
      sequence of whitespace characters delimited by whitespace), and advances the
      position to one character after the end of this token.

      's' is expected to be of type 'str' and 'pos' of type 'int'.
      This function returns a tuple
         (token, new_pos).
      If we're at the end of the string (there is only whitespace between 'pos' and
      the end), then 'token' will be None and 'pos' will be len(s).
   """
   assert isinstance(s, str) and isinstance(pos, int)
   assert pos >= 0
   # Skip over any initial whitespace.
   while pos < len(s) and s[pos].isspace():
      pos += 1
   if pos >= len(s):
      # We reached the end of the string s without finding any non-whitespace.
      return (None, pos)
   initial_pos = pos
   while pos < len(s) and not s[pos].isspace():
      pos += 1
   token = s[initial_pos:pos]
   return (token, pos)