Round widget coordinates to integers

[emilk]

Rounding errors in size calculation can lead to subtle layout bugs.

In particularly when auto-sizing an area, the size is usually the sum of the sizes of many smaller widgets and border margins. If we have rounding errors, we might next frame tell the inner widgets to have a slightly different size than last frame, which could potentially cause drastic changes, like word-breaking some text earlier (see #5161).

Integers up to 2^24 (4Mi) can be represented exactly using f32, so has no rounding errors when adding and subtracting them.
Using integers for layout coordinates therefore seems like a good idea.

This includes margin widths, etc.

To detect problems like these we first want to implement:

• Debug tool to highlight unaligned cursor coordinates #4927

Once that is in, we can start fixing these issues.

There is a sliding scale of how aggressively we enforce this.

Best-effort

Make sure all default egui widgets and margins are integers, and that centering layouts (etc) round to integers.

This means the whole egui_demo_app should end up with integer coordinates.

Ui-enforced

We could also have Ui round its cursor, allocated sizes etc to integers, basically pushing integer coordinates onto the user.

Switch from f32 to i32

This is the most aggressive stance, where we switch to integer coordinates everywhere.

I suspect this will be taking it too far because:

• It is a big undertaking
• It is a hugely breaking change
• We should still want to allow f32 for visual things (shapes), so it would requite having an Rectf and a Recti, Pos2f and Pos2i etc, and then have glue-code between the two everywhere

Round to integers or less?

We want to avoid rounding errors due to limited precision, but that doesn't mean we need to round to integers.

We could just as well round to 1/16ths, for instance, and still have plenty of precision in a f32.

The advantage of rounding to a fractional value is that we can get more fine-grained layouts, and smoother scrolling.

• See Round widgets to integer coordinates #5197 for more details

Rounding to ui points vs physical pixels

Rounding to ui points is the only thing that will prevent rounding errors.

Rounding to physical pixels still makes sense when rendering, i.e. to align text and other shapes to the physical pixel grid.
This however should not affect the layout, so it should be done either by the widgets before handing shapes to the painter, or automatically by the tessellator.

See #5164 for more

Related issues

• Add ui.align_cursor() to for the cursor to be aligned with physical pixels #4928
• Prevent text shrinking in tooltips; round wrap-width to integer #5161
• Align shapes to physical pixel grid #5164