int screen_width_mm();