#1859 Incorrect font size in auto-completoin list on GTK >= 3.21

[Colomban Wendling]

GTK 3.21.0 changed (fixed) font size handling, leading to properly interpreting pixels and points in CSS declarations. However, as older versions incorrectly handled those, the code has to handle both behaviours.

From CSS, GTK < 3.21.0 actually applied the conversion to points, but incorrectly: 10px was used as 10pt, but 10pt was scaled up twice.

So, assuming 96 DPI, it leads to:

font-size	3.20.0	3.21.0
10px	13.33px	10px
10pt	17.77px	13.33px

So, we need to fix the code to accommodate for both (either scaling ourselves, or adapting the unit: I chose the second, simpler, option).

See https://git.gnome.org/browse/gtk+/commit/?id=df08fc91bdc1d2e4c866122304fabe4dd298a7de

[Neil Hodgson]

Committed as [a4b5da].