*/
  public void prioritize_textures (int [] textures, float [] priorities) {
    RequestOutputStream o = display.out;
    synchronized (o) {
      begin_render_request (o, 4118, 8+textures.length*2*8);
      for (int i = 0; i < textures.length; i++)
        o.write_int32 (textures[i]);
      for (int i = 0; i < priorities.length; i++)
        o.write_float (priorities[i]);
    }
  }