module FF.CSS.Spec.Safe.Value.Multicol 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.Base using (RawValue; renderRawValue)
open import FF.CSS.Spec.Safe.Value.Color using (Color; renderColor)
open import FF.CSS.Spec.Safe.Value.Unit using
( Integer
; Length
; LengthPercentage
; renderInteger
; renderLength
; renderLengthPercentage
)
private
infixr 5 _++_
_++_ : String -> String -> String
_++_ = primStringAppend
data ColumnCount : Type lzero where
multicolCountAuto : ColumnCount
multicolCountInteger : Integer -> ColumnCount
renderColumnCount : ColumnCount -> String
renderColumnCount multicolCountAuto = "auto"
renderColumnCount (multicolCountInteger value) = renderInteger value
data ColumnFill : Type lzero where
multicolFillAuto multicolFillBalance : ColumnFill
renderColumnFill : ColumnFill -> String
renderColumnFill multicolFillAuto = "auto"
renderColumnFill multicolFillBalance = "balance"
data ColumnGap : Type lzero where
multicolGapNormal : ColumnGap
multicolGapLengthPercentage : LengthPercentage -> ColumnGap
renderColumnGap : ColumnGap -> String
renderColumnGap multicolGapNormal = "normal"
renderColumnGap (multicolGapLengthPercentage value) = renderLengthPercentage value
data MulticolLineWidth : Type lzero where
multicolLineThin multicolLineMedium multicolLineThick : MulticolLineWidth
multicolLineLength : Length -> MulticolLineWidth
renderMulticolLineWidth : MulticolLineWidth -> String
renderMulticolLineWidth multicolLineThin = "thin"
renderMulticolLineWidth multicolLineMedium = "medium"
renderMulticolLineWidth multicolLineThick = "thick"
renderMulticolLineWidth (multicolLineLength value) = renderLength value
data MulticolLineStyle : Type lzero where
multicolLineNone multicolLineHidden multicolLineDotted multicolLineDashed : MulticolLineStyle
multicolLineSolid multicolLineDouble multicolLineGroove multicolLineRidge : MulticolLineStyle
multicolLineInset multicolLineOutset : MulticolLineStyle
renderMulticolLineStyle : MulticolLineStyle -> String
renderMulticolLineStyle multicolLineNone = "none"
renderMulticolLineStyle multicolLineHidden = "hidden"
renderMulticolLineStyle multicolLineDotted = "dotted"
renderMulticolLineStyle multicolLineDashed = "dashed"
renderMulticolLineStyle multicolLineSolid = "solid"
renderMulticolLineStyle multicolLineDouble = "double"
renderMulticolLineStyle multicolLineGroove = "groove"
renderMulticolLineStyle multicolLineRidge = "ridge"
renderMulticolLineStyle multicolLineInset = "inset"
renderMulticolLineStyle multicolLineOutset = "outset"
record ColumnRuleWidthList : Type lzero where
constructor multicolRuleWidthList
field rawColumnRuleWidthList : RawValue
open ColumnRuleWidthList public
renderColumnRuleWidthList : ColumnRuleWidthList -> String
renderColumnRuleWidthList (multicolRuleWidthList value) = renderRawValue value
data ColumnRuleWidth : Type lzero where
multicolRuleWidthLine : MulticolLineWidth -> ColumnRuleWidth
renderColumnRuleWidth : ColumnRuleWidth -> String
renderColumnRuleWidth (multicolRuleWidthLine value) = renderMulticolLineWidth value
record ColumnRuleStyleList : Type lzero where
constructor multicolRuleStyleList
field rawColumnRuleStyleList : RawValue
open ColumnRuleStyleList public
renderColumnRuleStyleList : ColumnRuleStyleList -> String
renderColumnRuleStyleList (multicolRuleStyleList value) = renderRawValue value
data ColumnRuleStyle : Type lzero where
multicolRuleStyleLine : MulticolLineStyle -> ColumnRuleStyle
renderColumnRuleStyle : ColumnRuleStyle -> String
renderColumnRuleStyle (multicolRuleStyleLine value) = renderMulticolLineStyle value
ColumnRuleColor : Type lzero
ColumnRuleColor = Color
renderColumnRuleColor : ColumnRuleColor -> String
renderColumnRuleColor = renderColor
data ColumnRuleCore : Type lzero where
multicolRuleWidthOnly : MulticolLineWidth -> ColumnRuleCore
multicolRuleStyleOnly : MulticolLineStyle -> ColumnRuleCore
multicolRuleColorOnly : ColumnRuleColor -> ColumnRuleCore
multicolRuleWidthStyle : MulticolLineWidth -> MulticolLineStyle -> ColumnRuleCore
multicolRuleWidthColor : MulticolLineWidth -> ColumnRuleColor -> ColumnRuleCore
multicolRuleStyleColor : MulticolLineStyle -> ColumnRuleColor -> ColumnRuleCore
multicolRuleFull : MulticolLineWidth -> MulticolLineStyle -> ColumnRuleColor -> ColumnRuleCore
renderColumnRuleCore : ColumnRuleCore -> String
renderColumnRuleCore (multicolRuleWidthOnly width) = renderMulticolLineWidth width
renderColumnRuleCore (multicolRuleStyleOnly style) = renderMulticolLineStyle style
renderColumnRuleCore (multicolRuleColorOnly color) = renderColumnRuleColor color
renderColumnRuleCore (multicolRuleWidthStyle width style) =
renderMulticolLineWidth width ++ " " ++ renderMulticolLineStyle style
renderColumnRuleCore (multicolRuleWidthColor width color) =
renderMulticolLineWidth width ++ " " ++ renderColumnRuleColor color
renderColumnRuleCore (multicolRuleStyleColor style color) =
renderMulticolLineStyle style ++ " " ++ renderColumnRuleColor color
renderColumnRuleCore (multicolRuleFull width style color) =
renderMulticolLineWidth width ++ " " ++ renderMulticolLineStyle style ++ " " ++ renderColumnRuleColor color
record ColumnRuleList : Type lzero where
constructor multicolRuleList
field rawColumnRuleList : RawValue
open ColumnRuleList public
renderColumnRuleList : ColumnRuleList -> String
renderColumnRuleList (multicolRuleList value) = renderRawValue value
data ColumnRule : Type lzero where
multicolRuleCore : ColumnRuleCore -> ColumnRule
renderColumnRule : ColumnRule -> String
renderColumnRule (multicolRuleCore value) = renderColumnRuleCore value
data ColumnSpan : Type lzero where
multicolSpanNone multicolSpanAll : ColumnSpan
renderColumnSpan : ColumnSpan -> String
renderColumnSpan multicolSpanNone = "none"
renderColumnSpan multicolSpanAll = "all"
data ColumnWidth : Type lzero where
multicolWidthAuto : ColumnWidth
multicolWidthLength : Length -> ColumnWidth
renderColumnWidth : ColumnWidth -> String
renderColumnWidth multicolWidthAuto = "auto"
renderColumnWidth (multicolWidthLength value) = renderLength value
data ColumnHeight : Type lzero where
multicolHeightAuto : ColumnHeight
multicolHeightLength : Length -> ColumnHeight
renderColumnHeight : ColumnHeight -> String
renderColumnHeight multicolHeightAuto = "auto"
renderColumnHeight (multicolHeightLength value) = renderLength value
data ColumnWrap : Type lzero where
multicolWrapAuto multicolWrapNowrap multicolWrapWrap : ColumnWrap
renderColumnWrap : ColumnWrap -> String
renderColumnWrap multicolWrapAuto = "auto"
renderColumnWrap multicolWrapNowrap = "nowrap"
renderColumnWrap multicolWrapWrap = "wrap"
data ColumnsBase : Type lzero where
multicolColumnsWidthOnly : ColumnWidth -> ColumnsBase
multicolColumnsCountOnly : ColumnCount -> ColumnsBase
multicolColumnsWidthCount : ColumnWidth -> ColumnCount -> ColumnsBase
multicolColumnsCountWidth : ColumnCount -> ColumnWidth -> ColumnsBase
renderColumnsBase : ColumnsBase -> String
renderColumnsBase (multicolColumnsWidthOnly width) = renderColumnWidth width
renderColumnsBase (multicolColumnsCountOnly count) = renderColumnCount count
renderColumnsBase (multicolColumnsWidthCount width count) =
renderColumnWidth width ++ " " ++ renderColumnCount count
renderColumnsBase (multicolColumnsCountWidth count width) =
renderColumnCount count ++ " " ++ renderColumnWidth width
data Columns : Type lzero where
multicolColumnsBase : ColumnsBase -> Columns
multicolColumnsWithHeight : ColumnsBase -> ColumnHeight -> Columns
renderColumns : Columns -> String
renderColumns (multicolColumnsBase value) = renderColumnsBase value
renderColumns (multicolColumnsWithHeight value height) =
renderColumnsBase value ++ " / " ++ renderColumnHeight height
data MulticolPropertyName : Type lzero where
multicolColumnCountProp multicolColumnFillProp multicolColumnGapProp : MulticolPropertyName
multicolColumnRuleColorProp multicolColumnRuleStyleProp multicolColumnRuleWidthProp : MulticolPropertyName
multicolColumnRuleProp multicolColumnSpanProp multicolColumnWidthProp multicolColumnHeightProp multicolColumnWrapProp multicolColumnsProp : MulticolPropertyName
renderMulticolPropertyName : MulticolPropertyName -> String
renderMulticolPropertyName multicolColumnCountProp = "column-count"
renderMulticolPropertyName multicolColumnFillProp = "column-fill"
renderMulticolPropertyName multicolColumnGapProp = "column-gap"
renderMulticolPropertyName multicolColumnRuleColorProp = "column-rule-color"
renderMulticolPropertyName multicolColumnRuleStyleProp = "column-rule-style"
renderMulticolPropertyName multicolColumnRuleWidthProp = "column-rule-width"
renderMulticolPropertyName multicolColumnRuleProp = "column-rule"
renderMulticolPropertyName multicolColumnSpanProp = "column-span"
renderMulticolPropertyName multicolColumnWidthProp = "column-width"
renderMulticolPropertyName multicolColumnHeightProp = "column-height"
renderMulticolPropertyName multicolColumnWrapProp = "column-wrap"
renderMulticolPropertyName multicolColumnsProp = "columns"
data MulticolPropertyValue : MulticolPropertyName -> Type lzero where
multicolColumnCountValue : ColumnCount -> MulticolPropertyValue multicolColumnCountProp
multicolColumnFillValue : ColumnFill -> MulticolPropertyValue multicolColumnFillProp
multicolColumnGapValue : ColumnGap -> MulticolPropertyValue multicolColumnGapProp
multicolColumnRuleColorValue : ColumnRuleColor -> MulticolPropertyValue multicolColumnRuleColorProp
multicolColumnRuleStyleValue : ColumnRuleStyle -> MulticolPropertyValue multicolColumnRuleStyleProp
multicolColumnRuleWidthValue : ColumnRuleWidth -> MulticolPropertyValue multicolColumnRuleWidthProp
multicolColumnRuleValue : ColumnRule -> MulticolPropertyValue multicolColumnRuleProp
multicolColumnSpanValue : ColumnSpan -> MulticolPropertyValue multicolColumnSpanProp
multicolColumnWidthValue : ColumnWidth -> MulticolPropertyValue multicolColumnWidthProp
multicolColumnHeightValue : ColumnHeight -> MulticolPropertyValue multicolColumnHeightProp
multicolColumnWrapValue : ColumnWrap -> MulticolPropertyValue multicolColumnWrapProp
multicolColumnsValue : Columns -> MulticolPropertyValue multicolColumnsProp
renderMulticolPropertyValue : (propertyName : MulticolPropertyName) -> MulticolPropertyValue propertyName -> String
renderMulticolPropertyValue multicolColumnCountProp (multicolColumnCountValue value) = renderColumnCount value
renderMulticolPropertyValue multicolColumnFillProp (multicolColumnFillValue value) = renderColumnFill value
renderMulticolPropertyValue multicolColumnGapProp (multicolColumnGapValue value) = renderColumnGap value
renderMulticolPropertyValue multicolColumnRuleColorProp (multicolColumnRuleColorValue value) = renderColumnRuleColor value
renderMulticolPropertyValue multicolColumnRuleStyleProp (multicolColumnRuleStyleValue value) = renderColumnRuleStyle value
renderMulticolPropertyValue multicolColumnRuleWidthProp (multicolColumnRuleWidthValue value) = renderColumnRuleWidth value
renderMulticolPropertyValue multicolColumnRuleProp (multicolColumnRuleValue value) = renderColumnRule value
renderMulticolPropertyValue multicolColumnSpanProp (multicolColumnSpanValue value) = renderColumnSpan value
renderMulticolPropertyValue multicolColumnWidthProp (multicolColumnWidthValue value) = renderColumnWidth value
renderMulticolPropertyValue multicolColumnHeightProp (multicolColumnHeightValue value) = renderColumnHeight value
renderMulticolPropertyValue multicolColumnWrapProp (multicolColumnWrapValue value) = renderColumnWrap value
renderMulticolPropertyValue multicolColumnsProp (multicolColumnsValue value) = renderColumns value
record MulticolPropertyPair : Type lzero where
constructor multicolPair
field
multicolPairName : MulticolPropertyName
multicolPairValue : MulticolPropertyValue multicolPairName
open MulticolPropertyPair public
renderMulticolPropertyPair : MulticolPropertyPair -> String
renderMulticolPropertyPair (multicolPair propertyName value) =
renderMulticolPropertyName propertyName ++ ": " ++ renderMulticolPropertyValue propertyName value