
   0 | module Text.CSS.Property
   1 | 
   2 | import Data.List
   3 | import Data.String
   4 | import Data.Vect
   5 | import Text.CSS.Color
   6 | import Text.CSS.Dir
   7 | import Text.CSS.Flexbox
   8 | import Text.CSS.Grid
   9 | import Text.CSS.Length
  10 | import Text.CSS.ListStyleType
  11 | import Text.CSS.Percentage
  12 | 
  13 | %default total
  14 | 
  15 | namespace BoxSizing
  16 |   public export
  17 |   data BoxSizing = BorderBox | ContentBox
  18 | 
  19 |   export
  20 |   Interpolation BoxSizing where
  21 |     interpolate BorderBox  = "border-box"
  22 |     interpolate ContentBox = "content-box"
  23 | 
  24 | namespace Direction
  25 |   public export
  26 |   data Direction = LTR | RTL
  27 | 
  28 |   export
  29 |   Interpolation Direction where
  30 |     interpolate LTR = "ltr"
  31 |     interpolate RTL = "rtl"
  32 | 
  33 | namespace Display
  34 |   public export
  35 |   interface AreaTag a where
  36 |     showTag : a -> String
  37 | 
  38 |   public export
  39 |   data Display : Type where
  40 |     Flex  : Display
  41 |     Grid  : Display
  42 |     Area  :  {0 n,m : Nat}
  43 |           -> {0 a : Type}
  44 |           -> AreaTag a
  45 |           => (rows    : Vect (S m) GridValue)
  46 |           -> (columns : Vect (S n) GridValue)
  47 |           -> (area    : Vect (S m) (Vect (S n) a))
  48 |           -> Display
  49 | 
  50 |   export
  51 |   renderArea :
  52 |        {auto _ : AreaTag a}
  53 |     -> Vect (S m) GridValue
  54 |     -> Vect (S n) GridValue
  55 |     -> Vect (S m) (Vect (S n) a)
  56 |     -> String
  57 |   renderArea rs cs as =
  58 |     let rsStr := "grid-template-rows: \{toList rs}"
  59 |         csStr := "grid-template-columns: \{toList cs}"
  60 |         aStr  := fastConcat . intersperse " " . map col $ toList as
  61 |      in "display: grid; \{rsStr}; \{csStr}; grid-template-areas: \{aStr}"
  62 | 
  63 |     where
  64 |       col : Vect (S n) a -> String
  65 |       col vs =
  66 |         let str := concat . intersperse " " . map showTag $ toList vs
  67 |          in #""\#{str}""#
  68 | 
  69 | namespace FlexBasis
  70 |   public export
  71 |   data FlexBasis : Type where
  72 |     FL       : Length -> FlexBasis
  73 |     FP       : Percentage -> FlexBasis
  74 | 
  75 |   export
  76 |   Interpolation FlexBasis where
  77 |     interpolate (FL x)   = interpolate x
  78 |     interpolate (FP x)   = interpolate x
  79 | 
  80 |   export %inline
  81 |   Cast Length FlexBasis where
  82 |     cast = FL
  83 | 
  84 |   export %inline
  85 |   Cast Percentage FlexBasis where
  86 |     cast = FP
  87 | 
  88 | namespace FontSize
  89 |   public export
  90 |   data FontSize : Type where
  91 |     FL       : Length -> FontSize
  92 |     FP       : Percentage -> FontSize
  93 |     XXSmall  : FontSize
  94 |     XSmall   : FontSize
  95 |     Small    : FontSize
  96 |     Medium   : FontSize
  97 |     Large    : FontSize
  98 |     XLarge   : FontSize
  99 |     XXLarge  : FontSize
 100 |     XXXLarge : FontSize
 101 | 
 102 |   export
 103 |   Interpolation FontSize where
 104 |     interpolate (FL x)   = interpolate x
 105 |     interpolate (FP x)   = interpolate x
 106 |     interpolate XXSmall  = "xx-small"
 107 |     interpolate XSmall   = "x-small"
 108 |     interpolate Small    = "small"
 109 |     interpolate Medium   = "medium"
 110 |     interpolate Large    = "large"
 111 |     interpolate XLarge   = "x-large"
 112 |     interpolate XXLarge  = "xx-large"
 113 |     interpolate XXXLarge = "xxx-large"
 114 | 
 115 |   export %inline
 116 |   Cast Length FontSize where
 117 |     cast = FL
 118 | 
 119 |   export %inline
 120 |   Cast Percentage FontSize where
 121 |     cast = FP
 122 | 
 123 | namespace FontWeight
 124 |   public export
 125 |   data FontWeight : Type where
 126 |     Normal  : FontWeight
 127 |     Bold    : FontWeight
 128 |     Lighter : FontWeight
 129 |     Bolder  : FontWeight
 130 |     FW100   : FontWeight
 131 |     FW200   : FontWeight
 132 |     FW300   : FontWeight
 133 |     FW400   : FontWeight
 134 |     FW500   : FontWeight
 135 |     FW600   : FontWeight
 136 |     FW700   : FontWeight
 137 |     FW800   : FontWeight
 138 |     FW900   : FontWeight
 139 | 
 140 |   export
 141 |   Interpolation FontWeight where
 142 |     interpolate Normal  = "normal"
 143 |     interpolate Bold    = "bold"
 144 |     interpolate Lighter = "lighter"
 145 |     interpolate Bolder  = "bolder"
 146 |     interpolate FW100   = "100"
 147 |     interpolate FW200   = "200"
 148 |     interpolate FW300   = "300"
 149 |     interpolate FW400   = "400"
 150 |     interpolate FW500   = "500"
 151 |     interpolate FW600   = "600"
 152 |     interpolate FW700   = "700"
 153 |     interpolate FW800   = "800"
 154 |     interpolate FW900   = "900"
 155 | 
 156 | namespace BorderRadius
 157 |   public export
 158 |   data BorderRadius : Type where
 159 |     BL : Length -> BorderRadius
 160 |     BP : Percentage -> BorderRadius
 161 |     BS : String -> BorderRadius
 162 | 
 163 |   export
 164 |   Interpolation BorderRadius where
 165 |     interpolate (BL x) = interpolate x
 166 |     interpolate (BP x) = interpolate x
 167 |     interpolate (BS x) = x
 168 | 
 169 |   export %inline
 170 |   Cast Length BorderRadius where
 171 |     cast = BL
 172 | 
 173 |   export %inline
 174 |   Cast Percentage BorderRadius where
 175 |     cast = BP
 176 | 
 177 |   export %inline
 178 |   FromString BorderRadius where
 179 |     fromString = BS
 180 | 
 181 | namespace BorderStyle
 182 |   public export
 183 |   data BorderStyle : Type where
 184 |     None   : BorderStyle
 185 |     Hidden : BorderStyle
 186 |     Dotted : BorderStyle
 187 |     Dashed : BorderStyle
 188 |     Solid  : BorderStyle
 189 |     Dbl    : BorderStyle
 190 |     Groove : BorderStyle
 191 |     Ridge  : BorderStyle
 192 |     Inset  : BorderStyle
 193 |     Outset : BorderStyle
 194 | 
 195 | 
 196 |   export
 197 |   Interpolation BorderStyle where
 198 |     interpolate None   = "none"
 199 |     interpolate Hidden = "hidden"
 200 |     interpolate Dotted = "dotted"
 201 |     interpolate Dashed = "dashed"
 202 |     interpolate Solid  = "solid"
 203 |     interpolate Dbl    = "double"
 204 |     interpolate Groove = "groove"
 205 |     interpolate Ridge  = "ridge"
 206 |     interpolate Inset  = "inset"
 207 |     interpolate Outset = "outset"
 208 | 
 209 | namespace BorderWidth
 210 |   public export
 211 |   data BorderWidth : Type where
 212 |     BL     : Length -> BorderWidth
 213 |     Thin   : BorderWidth
 214 |     Medium : BorderWidth
 215 |     Thick  : BorderWidth
 216 | 
 217 |   export
 218 |   Interpolation BorderWidth where
 219 |     interpolate (BL x) = interpolate x
 220 |     interpolate Thin   = "thin"
 221 |     interpolate Medium = "medium"
 222 |     interpolate Thick  = "thick"
 223 | 
 224 |   export %inline
 225 |   Cast Length BorderWidth where
 226 |     cast = BL
 227 | 
 228 | namespace Overflow
 229 | 
 230 |   ||| The `overflow-x` and `overflow-y` CSS properties set
 231 |   ||| what shows when content overflows a block-level element's
 232 |   ||| edges. This may be nothing, a scroll bar,
 233 |   ||| or the overflow content.
 234 |   public export
 235 |   data Overflow : Type where
 236 | 
 237 |     ||| Content is not clipped and may be rendered outside the padding box's edges.
 238 |     Visible : Overflow
 239 | 
 240 |     ||| Content is clipped if necessary to fit horizontally
 241 |     ||| in the padding box. No scrollbars are provided.
 242 |     ||| Programmatic scrolling is still possible.
 243 |     Hidden  : Overflow
 244 | 
 245 |     ||| Like `Hidden` but forbidding also programmatic scrolling.
 246 |     Clip    : Overflow
 247 | 
 248 |     ||| Content is clipped if necessary to fit in the padding box.
 249 |     ||| Browsers display scrollbars whether or not any content is actually clipped.
 250 |     ||| (This prevents scrollbars from appearing or disappearing when the
 251 |     ||| content changes.)
 252 |     Scroll  : Overflow
 253 | 
 254 |     ||| Depends on the user agent. If content fits inside the
 255 |     ||| padding box, it looks the same as visible, but still
 256 |     ||| establishes a new block-formatting context. Desktop browsers
 257 |     ||| provide scrollbars if content overflows.
 258 |     Auto    : Overflow
 259 | 
 260 |   export
 261 |   Interpolation Overflow where
 262 |     interpolate Visible = "visible"
 263 |     interpolate Hidden  = "hidden"
 264 |     interpolate Clip    = "clip"
 265 |     interpolate Scroll  = "scroll"
 266 |     interpolate Auto    = "auto"
 267 | 
 268 | namespace TextAlign
 269 |   public export
 270 |   data TextAlign : Type where
 271 |     ||| The same as left if direction is left-to-right and right if direction is right-to-left.
 272 |     Start   : TextAlign
 273 |     ||| The same as right if direction is left-to-right and left if direction is right-to-left.
 274 |     End     : TextAlign
 275 |     ||| The inline contents are aligned to the left edge of the line box.
 276 |     Left    : TextAlign
 277 |     ||| The inline contents are aligned to the right edge of the line box.
 278 |     Right   : TextAlign
 279 |     ||| The inline contents are centered within the line box.
 280 |     Center  : TextAlign
 281 |     ||| The inline contents are justified. Text should be spaced to line up its left and right edges to the left and right edges of the line box, except for the last line.
 282 |     Justify : TextAlign
 283 | 
 284 |   export
 285 |   Interpolation TextAlign where
 286 |     interpolate Start   = "start"
 287 |     interpolate End     = "end"
 288 |     interpolate Left    = "left"
 289 |     interpolate Right   = "right"
 290 |     interpolate Center  = "center"
 291 |     interpolate Justify = "justify"
 292 | 
 293 | namespace TextDecorationLine
 294 | 
 295 |   public export
 296 |   data TextDecorationLine : Type where
 297 |     None        : TextDecorationLine
 298 |     Underline   : TextDecorationLine
 299 |     Overline    : TextDecorationLine
 300 |     LineThrough : TextDecorationLine
 301 | 
 302 |   export
 303 |   Interpolation TextDecorationLine where
 304 |     interpolate None        = "none"
 305 |     interpolate Underline   = "underline"
 306 |     interpolate Overline    = "overline"
 307 |     interpolate LineThrough = "line-through"
 308 | 
 309 | namespace TextDecorationStyle
 310 | 
 311 |   public export
 312 |   data TextDecorationStyle : Type where
 313 |     Solid  : TextDecorationStyle
 314 |     Dbl    : TextDecorationStyle
 315 |     Dotted : TextDecorationStyle
 316 |     Dashed : TextDecorationStyle
 317 |     Wavy   : TextDecorationStyle
 318 | 
 319 |   export
 320 |   Interpolation TextDecorationStyle where
 321 |     interpolate Solid  = "solid"
 322 |     interpolate Dbl    = "double"
 323 |     interpolate Dotted = "dotted"
 324 |     interpolate Dashed = "dashed"
 325 |     interpolate Wavy   = "wavy"
 326 | 
 327 | namespace TextOverflow
 328 |   public export
 329 |   data TextOverflow = Clip | Ellipsis
 330 | 
 331 |   export
 332 |   Interpolation TextOverflow where
 333 |     interpolate Clip     = "clip"
 334 |     interpolate Ellipsis = "ellipsis"
 335 | 
 336 | namespace Width
 337 |   public export
 338 |   data Width : Type where
 339 |     WL       : Length -> Width
 340 |     WP       : Percentage -> Width
 341 | 
 342 |   export
 343 |   Interpolation Width where
 344 |     interpolate (WL x)   = interpolate x
 345 |     interpolate (WP x)   = interpolate x
 346 | 
 347 |   export %inline
 348 |   Cast Length Width where
 349 |     cast = WL
 350 | 
 351 |   export %inline
 352 |   Cast Percentage Width where
 353 |     cast = WP
 354 | 
 355 | namespace WiteSpace
 356 | 
 357 |   ||| Handles white space inside an element
 358 |   public export
 359 |   data WhiteSpace : Type where
 360 |     ||| White space is collapsed (several white space characters
 361 |     ||| are treated as a single space character) and lines are
 362 |     ||| broken as necessary.
 363 |     Normal      : WhiteSpace
 364 | 
 365 |     ||| Like `Normal` but suppresses line breaks (text wrapping)
 366 |     Nowrap      : WhiteSpace
 367 | 
 368 |     ||| Sequences of white space are preserved. Lines are broken at
 369 |     ||| newline characters and at `<br>` elements.
 370 |     Pre         : WhiteSpace
 371 | 
 372 |     ||| Sequences of white space are preserved. Lines are broken at
 373 |     ||| newline characters, at `<br>` elements, and as necessary
 374 |     ||| to fill the box.
 375 |     PreWrap     : WhiteSpace
 376 | 
 377 |     ||| Like `PreWrap` but collapses sequences of white space.
 378 |     PreLine     : WhiteSpace
 379 | 
 380 |     ||| The behavior is identical to that of `PreWrap`, except that:
 381 |     |||
 382 |     ||| * Any sequence of preserved white space always takes up space,
 383 |     |||   including at the end of the line.
 384 |     ||| * A line breaking opportunity exists after every preserved
 385 |     |||   white space character, including between white space characters.
 386 |     ||| * Such preserved spaces take up space and do not hang,
 387 |     |||   and thus affect the box's intrinsic sizes
 388 |     |||   (min-content size and max-content size).
 389 |     BreakSpaces : WhiteSpace
 390 | 
 391 |   export
 392 |   Interpolation WhiteSpace where
 393 |     interpolate Normal      = "normal"
 394 |     interpolate Nowrap      = "nowrap"
 395 |     interpolate Pre         = "pre"
 396 |     interpolate PreWrap     = "pre-wrap"
 397 |     interpolate PreLine     = "pre-line"
 398 |     interpolate BreakSpaces = "break-spaces"
 399 |