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