if (isSet(opts, IGNORE_CASE)) {
                          tok = tok.getCaseInsensitiveToken();
                          if (!tok.match(ch)) {
                              if (ch >= 0x10000)  return -1;
                              char uch;
                              if (!tok.match(uch = Character.toUpperCase((char)ch))
                                  && !tok.match(Character.toLowerCase(uch)))
                                  return -1;
                          }
                      } else {