boolean INTEGER_token_p(String str)
  /*
   * Does NOT recognize an isolated '+' or '-' as an integer.
   */
  {
    String INTchars = "0123456789";

    int   length = str.length();
    int   index  = 0;

    try {
      if ((index < length) && ((str.charAt(index) == '-') || (str.charAt(index) == '+')))
        index++;
    }
    catch (StringIndexOutOfBoundsException e) {
      System.err.println("Hey, got a bad string index in 'INTEGER_token_p'! on string '" + str + "'"); 
    }

    if (index == length)   // Don't accept a single '-' or '+'
      return false;

    return(SymbolTools.firstCharNotInSet(index, str, INTchars) == length);
  }