void SkipWhiteSpace(void) {

  char ch;

  while ((ch = ReadSymbol()) == ' ' || ch == '\n' || ch == '\t')
    ;

  /* if we read a character that wasn't whitespace
   * then we need to put it back
   */
  if (ch != ' ')
    UnReadSymbol(ch);
}