public void pushBack( int c ) throws IOException {
        if( debug ) {
            if( c == 0x0a ) {
                System.out.print("(<0x0a)");
            } else if( c == 0x0d ) {
                System.out.print("(<0x0d)");
            } else if( c == 0x09 ) {
                System.out.print("(<0x09)");
            } else {
                System.out.print("(<" + (char)c + ")");
            }            
        }
        reader.unread(c);
        column--;

        if( c == '\n' ) {
            // We partially deal with linefeed pushbacks
            // here with some caveats.  The biggest one is
            // that the column is temporarily incorrect because
            // it goes invalid.  When the character is read again
            // it will catch up, of course, but right after the
            // pushback the line is incorrect.
            line--;
        }            
    }