DPI aware font size in log windows: fix issue #76

This commit is contained in:
Vadim Lopatin 2015-03-23 11:40:00 +03:00
parent f511ba03ff
commit 865eaab4cb
2 changed files with 12 additions and 2 deletions

View File

@ -207,6 +207,16 @@ Rect toPixels(const Rect sz) {
return Rect(toPixels(sz.left), toPixels(sz.top), toPixels(sz.right), toPixels(sz.bottom));
}
/// make size value with SIZE_IN_POINTS_FLAG set
int makePointSize(int pt) {
return pt | SIZE_IN_POINTS_FLAG;
}
/// make size value with SIZE_IN_PERCENTS_FLAG set
int makePercentSize(int percent) {
return (percent * 100) | SIZE_IN_PERCENTS_FLAG;
}
/// screen dots per inch
private __gshared int PRIVATE_SCREEN_DPI = 96;

View File

@ -2371,11 +2371,11 @@ class LogWidget : EditBox {
_scrollLock = true;
_enableScrollAfterText = false;
enabled = false;
fontSize = 14;
fontSize = makePointSize(9);
//fontFace = "Consolas,Lucida Console,Courier New";
fontFace = "Consolas,DejaVuSansMono,Lucida Sans Typewriter,Courier New,Lucida Console";
fontFamily = FontFamily.MonoSpace;
minFontSize(8).maxFontSize(32); // allow font zoom with Ctrl + MouseWheel
minFontSize(pointsToPixels(6)).maxFontSize(pointsToPixels(32)); // allow font zoom with Ctrl + MouseWheel
onThemeChanged();
}