use_pixel_ - Pixel size property
When the property is set to true, pixel size is used instead of point size, which is used in case the property has been set to false. Pixel size makes the font device dependent.
Options.GUIFramework.Fonts._std_font.is_pixel=NO
Type: bool