Module ui.size
This module provides a standardized set of sizes for use in widgets.
There are values for borders, margins, paddings, radii, and lines. Have a look at the code for full details. If you are considering to deviate from one of the defaults, please take a second to consider:
- Why you want to differ in the first place. We consciously strive toward consistency in the UI, which is typically valued higher than one pixel more or less in a specific context.
- If there really isn't anything close to what you want, whether it should be added to the arsenal of default sizes rather than as a local exception.
Usage:
local Size = require("ui/size")
local frame -- just an example widget
frame = FrameContainer:new{
radius = Size.radius.window,
bordersize = Size.border.window,
padding = Size.padding.default,
margin = Size.margin.default,
VerticalGroup:new{
-- etc
}
}