module FF.CSS.Spec.Safe.Value.Table where
open import Agda.Builtin.String using (String; primStringAppend)
open import Agda.Primitive using (lzero) renaming (Set to Type)
open import FF.CSS.Spec.Safe.Value.Unit using (Length; renderLength)
private
infixr 5 _++_
_++_ : String -> String -> String
_++_ = primStringAppend
data BorderCollapse : Type lzero where
borderCollapseSeparate borderCollapseCollapse : BorderCollapse
renderBorderCollapse : BorderCollapse -> String
renderBorderCollapse borderCollapseSeparate = "separate"
renderBorderCollapse borderCollapseCollapse = "collapse"
data BorderSpacing : Type lzero where
borderSpacingOne : Length -> BorderSpacing
borderSpacingTwo : Length -> Length -> BorderSpacing
renderBorderSpacing : BorderSpacing -> String
renderBorderSpacing (borderSpacingOne value) = renderLength value
renderBorderSpacing (borderSpacingTwo horizontal vertical) =
renderLength horizontal ++ " " ++ renderLength vertical
data CaptionSide : Type lzero where
captionSideTop captionSideBottom : CaptionSide
renderCaptionSide : CaptionSide -> String
renderCaptionSide captionSideTop = "top"
renderCaptionSide captionSideBottom = "bottom"
data EmptyCells : Type lzero where
emptyCellsShow emptyCellsHide : EmptyCells
renderEmptyCells : EmptyCells -> String
renderEmptyCells emptyCellsShow = "show"
renderEmptyCells emptyCellsHide = "hide"
data TableLayout : Type lzero where
tableLayoutAuto tableLayoutFixed : TableLayout
renderTableLayout : TableLayout -> String
renderTableLayout tableLayoutAuto = "auto"
renderTableLayout tableLayoutFixed = "fixed"