<html><body><div style="color:#000; background-color:#fff; font-family:times new roman, new york, times, serif;font-size:12pt"><div>Using the DrRacket nightly build for 2013-12-09, checkboxes in the Preferences dialog have the text clipped.</div><div><br></div><div style="color: rgb(0, 0, 0); font-size: 16px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">It appears as though there isn't enough space to fit the text on 1 line, so it renders 2 lines. However, the top of the 1st</div><div style="color: rgb(0, 0, 0); font-size: 16px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">line and bottom of the 2nd line is rendered outside the client area for the checkbox. This issue is not specific to DrRacket</div><div style="color: rgb(0, 0, 0); font-size: 16px; font-family: times new roman,new york,times,serif; background-color: transparent;
font-style: normal;">and can be reproduced using</div><div style="color: rgb(0, 0, 0); font-size: 16px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;"><br></div><div style="color: rgb(0, 0, 0); font-size: 16px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">#lang racket/gui<br>(define frame (new frame% [label "Example"]))<br><br>(define check-box (new check-box%<br> (parent frame)<br> (label "A check box with a really long label to see if it still works and does not truncate any
text.")<br> (value #t)))<br><br>(send frame show #t)</div><div style="color: rgb(0, 0, 0); font-size: 16px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;"><br></div><div style="color: rgb(0, 0, 0); font-size: 16px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">I think all of the following must be true to reproduce the issue:</div><div style="color: rgb(0, 0, 0); font-size: 16px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;"><br></div><div style="color: rgb(0, 0, 0); font-size: 16px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">* racket/gui later than 5.3.6;</div><div style="color: rgb(0, 0, 0);
font-size: 16px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">* run on Windows; and<br></div><div style="color: rgb(0, 0, 0); font-size: 16px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">* have DPI set larger than the Windows default.</div><div style="color: rgb(0, 0, 0); font-size: 16px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;"><br></div><div style="color: rgb(0, 0, 0); font-size: 16px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">Regarding the DPI issue, this can be changed via the 'Personalize' menu item from the Desktop and selecting the "Make text appear larger (125%)" item for example.</div><div style="color: rgb(0, 0, 0); font-size: 16px; font-family: times new roman,new york,times,serif; background-color:
transparent; font-style: normal;">A log off and on is required for the change to apply.</div><div style="color: rgb(0, 0, 0); font-size: 16px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;"><br></div><div style="color: rgb(0, 0, 0); font-size: 16px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">Broken example:</div><div style="color: rgb(0, 0, 0); font-size: 16px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">2013-12-09 nightly on Windows 7 with text set to 125%.</div><div style="color: rgb(0, 0, 0); font-size: 16px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;"><br></div><div style="color: rgb(0, 0, 0); font-size: 16px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">Working
examples:</div><div style="color: rgb(0, 0, 0); font-size: 16px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">5.3.6 on Windows 7 with text set to 125%.</div><div style="color: rgb(0, 0, 0); font-size: 16px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">2013-12-09 nightly on Windows 8 with text set to 100%</div><div style="color: rgb(0, 0, 0); font-size: 16px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">5.3.6 on Linux with GTK and default DPI</div><div style="color: rgb(0, 0, 0); font-size: 16px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">2013-12-09 nightly on Linux with GTK and default DPI</div><div style="color: rgb(0, 0, 0); font-size: 16px; font-family: times new roman,new york,times,serif; background-color: transparent;
font-style: normal;"><br></div><div style="color: rgb(0, 0, 0); font-size: 16px; font-family: times new roman,new york,times,serif; background-color: transparent; font-style: normal;">Regards</div></div></body></html>