private static char readChar() {  // return and discard next character from input
      char ch = lookChar();
      if (buffer == null) {
         if (readingStandardInput)
            throw new IllegalArgumentException("Attempt to read past end-of-file in standard input???");
         else
            throw new IllegalArgumentException("Attempt to read past end-of-file in file \"" + inputFileName + "\".");
      }
      pos++;
      return ch;
   }