void write(DataOutputStream out) throws IOException {
        int len = size();
        out.writeShort(len);            // exception_table_length
        for (int i = 0; i < len; ++i) {
            ExceptionTableEntry e = (ExceptionTableEntry)entries.get(i);
            out.writeShort(e.startPc);
            out.writeShort(e.endPc);
            out.writeShort(e.handlerPc);
            out.writeShort(e.catchType);
        }
    }