private void flush_render_request () {
    RequestOutputStream o = display.out;
    if (o.index > 0 && o.opcode () == 1) {
      o.update_length ();
      o.flush ();
    }
  }

//  private Enum read_enum (Request request) {
//    Data reply = display.read_reply (request);
//    int n = reply.read4 (12);
//    
//    if (n == 0) return null;
//    if (n == 1) return new Enum (reply, 16, 1);
//    return new Enum (reply, 32, n);
//  }