From e45cd43aaab7af014607b2578ec68a5bbec1b609 Mon Sep 17 00:00:00 2001 From: Ben Harris Date: Mon, 7 Nov 2022 21:42:38 +0000 Subject: Teach the mid-end about device pixel ratios The device pixel ratio indicates how many physical pixels there are in the platonic ideal of a pixel, at least approximately. In Web browsers, the device pixel ratio is used to represent "retina" displays with particularly high pixel densities, and also to reflect user-driven zooming of the page to different text sizes. The mid-end uses the device pixel ratio to adjust the tile size at startup, and can also respond to changes in device pixel ratio by adjusting the time size later. This is accomplished through a new argument to midend_size() which can simply be passed as 1.0 in any front end that doesn't care about this. --- nestedvm.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'nestedvm.c') diff --git a/nestedvm.c b/nestedvm.c index 947abe0..ec633d3 100644 --- a/nestedvm.c +++ b/nestedvm.c @@ -217,7 +217,7 @@ int jcallback_resize(int width, int height) int x, y; x = width; y = height; - midend_size(fe->me, &x, &y, true); + midend_size(fe->me, &x, &y, true, 1.0); fe->ox = (width - x) / 2; fe->oy = (height - y) / 2; fe->w = x; @@ -358,7 +358,7 @@ static void resize_fe(frontend *fe) x = INT_MAX; y = INT_MAX; - midend_size(fe->me, &x, &y, false); + midend_size(fe->me, &x, &y, false, 1.0); _call_java(3, x, y, 0); } -- cgit v1.1