2022-06-11 21:09:14 +00:00
|
|
|
-- Div (Division, like in HTML) Graphics Element
|
|
|
|
|
|
|
|
local element = require("graphics.element")
|
|
|
|
|
|
|
|
---@class div_args
|
|
|
|
---@field parent graphics_element
|
2022-07-28 14:09:34 +00:00
|
|
|
---@field id? string element id
|
2022-06-11 21:09:14 +00:00
|
|
|
---@field x? integer 1 if omitted
|
|
|
|
---@field y? integer 1 if omitted
|
|
|
|
---@field width? integer parent width if omitted
|
|
|
|
---@field height? integer parent height if omitted
|
|
|
|
---@field gframe? graphics_frame frame instead of x/y/width/height
|
|
|
|
---@field fg_bg? cpair foreground/background colors
|
|
|
|
|
|
|
|
-- new div element
|
2023-02-25 00:50:01 +00:00
|
|
|
---@nodiscard
|
2022-06-11 21:09:14 +00:00
|
|
|
---@param args div_args
|
2022-07-28 14:09:34 +00:00
|
|
|
---@return graphics_element element, element_id id
|
2022-06-11 21:09:14 +00:00
|
|
|
local function div(args)
|
|
|
|
-- create new graphics element base object
|
2022-07-28 15:17:34 +00:00
|
|
|
return element.new(args).get()
|
2022-06-11 21:09:14 +00:00
|
|
|
end
|
|
|
|
|
|
|
|
return div
|