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
|
2023-07-10 03:42:44 +00:00
|
|
|
---@field y? integer auto incremented if omitted
|
2022-06-11 21:09:14 +00:00
|
|
|
---@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
|
2023-05-25 21:40:16 +00:00
|
|
|
---@field hidden? boolean true to hide on initial draw
|
2022-06-11 21:09:14 +00:00
|
|
|
|
|
|
|
-- 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
|
2023-05-30 23:51:10 +00:00
|
|
|
return element.new(args).complete()
|
2022-06-11 21:09:14 +00:00
|
|
|
end
|
|
|
|
|
|
|
|
return div
|