private int digit(int base) {
        char c = ch;
        int result = Character.digit(c, base);
        if (result >= 0 && c > 0x7f) {
            ch = "0123456789abcdef".charAt(result);
        }
        return result;
    }