if (c > 0x07FF) {
        ch = (char)(c >>> 12);
        write = 0xE0;
        if (ch > 0) {
          write |= (ch & 0x0F);