public static void unreadCharacterFromTokenizerBuffer(char renamed_Char, InputStream stream) {
    { TokenizerStreamState state = stream.tokenizerState;
      int cursor = state.cursor;

      if (cursor == 0) {
        cursor = state.bufferSize - 1;
      }
      else {
        cursor = cursor - 1;
      }
      if (!(renamed_Char == ((char) (0x00ff & (state.buffer)[cursor])))) {
        { OutputStringStream stream000 = OutputStringStream.newOutputStringStream();

          stream000.nativeStream.print("Unread character `" + renamed_Char + "' does not match last character read");
          throw ((StellaException)(StellaException.newStellaException(stream000.theStringReader()).fillInStackTrace()));
        }
      }
      state.cursor = cursor;
    }
  }