private static void skipWhitespace() {
      char ch=lookChar();
      while (ch != EOF && Character.isWhitespace(ch)) {
         readChar();
         if (ch == '\n' && readingStandardInput && writingStandardOutput) {
            out.print("? ");
            out.flush();
         }
         ch = lookChar();
      }
   }