After this change, UserInterface's windowWidth and windowHeight are now windowWidthInDP and windowHeightInDP in device-independent pixels. Closes #1844