<br><br><div class="gmail_quote">On Thu, Jul 22, 2010 at 14:51, Matthew Flatt <span dir="ltr">&lt;<a href="mailto:mflatt@cs.utah.edu">mflatt@cs.utah.edu</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">

<div><div></div><div class="h5">At Thu, 22 Jul 2010 10:26:47 +0200, Laurent wrote:<br>
&gt; I can see there is a `get-panel-background&#39; function that returns the<br>
&gt; background color of panels, but is there a `set-panel-background&#39; or<br>
&gt; something equivalent?<br>
<br>
</div></div>No, there&#39;s no way currently to set the background of a panel.<br>
<br>
Even `get-panel-background&#39; isn&#39;t really a good idea, since the<br>
graphical depiction of the panel is up to the GUI toolkit and maybe<br>
some user-selected theme, and it isn&#39;t necessarily just a color.<br></blockquote><div><br>Right. Though the color (gray) does not seem to match my desktop theme (more like yellow) on Ubuntu. That would be perfect if the panels in my GUI matched my desktop theme, but I suspect this is not what you&#39;re saying?<br>

 </div><blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
<br>
After GRacket moves to more modern GUI toolkits, we&#39;ll revisit<br>
questions like this, based on what the toolkits provide.<br></blockquote><div><br>Can&#39;t wait for this!<br>Do you have an idea of when you may finish it? <br></div></div>