*/
  public void color3d (double red, double green, double blue) {
    RequestOutputStream o = display.out;
    synchronized (o) {
      begin_render_request (o, 7, 28);
      o.write_double (red);
      o.write_double (green);
      o.write_double (blue);
    }
  }