
   0 | module Text.CSS.Property
   1 | 
   2 | import Data.List
   3 | import Data.String
   4 | import Data.Vect
   5 | import Text.CSS.Angle
   6 | import Text.CSS.Color
   7 | import Text.CSS.Dir
   8 | import Text.CSS.Flexbox
   9 | import Text.CSS.Grid
  10 | import Text.CSS.Length
  11 | import Text.CSS.ListStyleType
  12 | import Text.CSS.Percentage
  13 | 
  14 | %default total
  15 | 
  16 | namespace BoxSizing
  17 |   public export
  18 |   data BoxSizing = BorderBox | ContentBox
  19 | 
  20 |   export
  21 |   Interpolation BoxSizing where
  22 |     interpolate BorderBox  = "border-box"
  23 |     interpolate ContentBox = "content-box"
  24 | 
  25 | namespace ContainerType
  26 |   public export
  27 |   data ContainerType : Type where
  28 |     Normal                : ContainerType
  29 |     Size                  : ContainerType
  30 |     InlineSize            : ContainerType
  31 |     ScrollState           : ContainerType
  32 |     ScrollStateSize       : ContainerType
  33 |     ScrollStateInlineSize : ContainerType
  34 |     Anchored              : ContainerType
  35 | 
  36 |   export
  37 |   Interpolation ContainerType where
  38 |     interpolate Normal                = "normal"
  39 |     interpolate Size                  = "size"
  40 |     interpolate InlineSize            = "inline-size"
  41 |     interpolate ScrollState           = "scroll-state"
  42 |     interpolate ScrollStateSize       = "scroll-state size"
  43 |     interpolate ScrollStateInlineSize = "scroll-state inline-size"
  44 |     interpolate Anchored              = "anchor"
  45 | 
  46 | namespace Direction
  47 |   public export
  48 |   data Direction = LTR | RTL
  49 | 
  50 |   export
  51 |   Interpolation Direction where
  52 |     interpolate LTR = "ltr"
  53 |     interpolate RTL = "rtl"
  54 | 
  55 | namespace Display
  56 |   public export
  57 |   data Display : Type where
  58 |     None  : Display
  59 |     InlineBlock  : Display
  60 |     Flex  : Display
  61 |     Grid  : Display
  62 |     Area  :  {0 n,m : Nat}
  63 |           -> {0 a : Type}
  64 |           -> {auto as : Show a}
  65 |           -> (rows    : Vect (S m) GridValue)
  66 |           -> (columns : Vect (S n) GridValue)
  67 |           -> (area    : Vect (S m) (Vect (S n) a))
  68 |           -> Display
  69 | 
  70 |   export
  71 |   showTag : Show a => a -> String
  72 |   showTag v =
  73 |     case toLower $ show v of
  74 |       "dot" => "."
  75 |       s     => s
  76 | 
  77 |   col : Show a => Vect (S n) a -> String
  78 |   col vs =
  79 |     let s := concat . intersperse " " . map showTag $ toList vs
  80 |      in #""\#{s}""#
  81 | 
  82 |   export
  83 |   renderArea :
  84 |        {auto _ : Show a}
  85 |     -> Vect (S m) GridValue
  86 |     -> Vect (S n) GridValue
  87 |     -> Vect (S m) (Vect (S n) a)
  88 |     -> String
  89 |   renderArea rs cs as =
  90 |     let rsStr := "grid-template-rows: \{toList rs}"
  91 |         csStr := "grid-template-columns: \{toList cs}"
  92 |         aStr  := fastConcat . intersperse " " . map col $ toList as
  93 |      in "display: grid; \{rsStr}; \{csStr}; grid-template-areas: \{aStr}"
  94 | 
  95 | namespace FlexBasis
  96 |   public export
  97 |   data FlexBasis : Type where
  98 |     FL       : Length -> FlexBasis
  99 |     FP       : Percentage -> FlexBasis
 100 | 
 101 |   export
 102 |   Interpolation FlexBasis where
 103 |     interpolate (FL x)   = interpolate x
 104 |     interpolate (FP x)   = interpolate x
 105 | 
 106 |   export %inline
 107 |   Cast Length FlexBasis where
 108 |     cast = FL
 109 | 
 110 |   export %inline
 111 |   Cast Percentage FlexBasis where
 112 |     cast = FP
 113 | 
 114 | namespace FontSize
 115 |   public export
 116 |   data FontSize : Type where
 117 |     FL       : Length -> FontSize
 118 |     FP       : Percentage -> FontSize
 119 |     XXSmall  : FontSize
 120 |     XSmall   : FontSize
 121 |     Small    : FontSize
 122 |     Medium   : FontSize
 123 |     Large    : FontSize
 124 |     XLarge   : FontSize
 125 |     XXLarge  : FontSize
 126 |     XXXLarge : FontSize
 127 | 
 128 |   export
 129 |   Interpolation FontSize where
 130 |     interpolate (FL x)   = interpolate x
 131 |     interpolate (FP x)   = interpolate x
 132 |     interpolate XXSmall  = "xx-small"
 133 |     interpolate XSmall   = "x-small"
 134 |     interpolate Small    = "small"
 135 |     interpolate Medium   = "medium"
 136 |     interpolate Large    = "large"
 137 |     interpolate XLarge   = "x-large"
 138 |     interpolate XXLarge  = "xx-large"
 139 |     interpolate XXXLarge = "xxx-large"
 140 | 
 141 |   export %inline
 142 |   Cast Length FontSize where
 143 |     cast = FL
 144 | 
 145 |   export %inline
 146 |   Cast Percentage FontSize where
 147 |     cast = FP
 148 | 
 149 | namespace FontWeight
 150 |   public export
 151 |   data FontWeight : Type where
 152 |     Normal  : FontWeight
 153 |     Bold    : FontWeight
 154 |     Lighter : FontWeight
 155 |     Bolder  : FontWeight
 156 |     FW100   : FontWeight
 157 |     FW200   : FontWeight
 158 |     FW300   : FontWeight
 159 |     FW400   : FontWeight
 160 |     FW500   : FontWeight
 161 |     FW600   : FontWeight
 162 |     FW700   : FontWeight
 163 |     FW800   : FontWeight
 164 |     FW900   : FontWeight
 165 | 
 166 |   export
 167 |   Interpolation FontWeight where
 168 |     interpolate Normal  = "normal"
 169 |     interpolate Bold    = "bold"
 170 |     interpolate Lighter = "lighter"
 171 |     interpolate Bolder  = "bolder"
 172 |     interpolate FW100   = "100"
 173 |     interpolate FW200   = "200"
 174 |     interpolate FW300   = "300"
 175 |     interpolate FW400   = "400"
 176 |     interpolate FW500   = "500"
 177 |     interpolate FW600   = "600"
 178 |     interpolate FW700   = "700"
 179 |     interpolate FW800   = "800"
 180 |     interpolate FW900   = "900"
 181 | 
 182 | namespace FontStyle
 183 |   public export
 184 |   data FontStyle : Type where
 185 |     Normal   : FontStyle
 186 |     Italic   : FontStyle
 187 |     Oblique_ : FontStyle
 188 |     Oblique  : Angle -> FontStyle
 189 | 
 190 |   export
 191 |   Interpolation FontStyle where
 192 |     interpolate Normal      = "normal"
 193 |     interpolate Italic      = "italic"
 194 |     interpolate Oblique_    = "oblique"
 195 |     interpolate (Oblique x) = "oblique \{x}"
 196 | 
 197 | 
 198 | namespace BorderRadius
 199 |   public export
 200 |   data BorderRadius : Type where
 201 |     BL : Length -> BorderRadius
 202 |     BP : Percentage -> BorderRadius
 203 |     BS : String -> BorderRadius
 204 | 
 205 |   export
 206 |   Interpolation BorderRadius where
 207 |     interpolate (BL x) = interpolate x
 208 |     interpolate (BP x) = interpolate x
 209 |     interpolate (BS x) = x
 210 | 
 211 |   export %inline
 212 |   Cast Length BorderRadius where
 213 |     cast = BL
 214 | 
 215 |   export %inline
 216 |   Cast Percentage BorderRadius where
 217 |     cast = BP
 218 | 
 219 |   export %inline
 220 |   FromString BorderRadius where
 221 |     fromString = BS
 222 | 
 223 | namespace BorderStyle
 224 |   public export
 225 |   data BorderStyle : Type where
 226 |     None   : BorderStyle
 227 |     Hidden : BorderStyle
 228 |     Dotted : BorderStyle
 229 |     Dashed : BorderStyle
 230 |     Solid  : BorderStyle
 231 |     Dbl    : BorderStyle
 232 |     Groove : BorderStyle
 233 |     Ridge  : BorderStyle
 234 |     Inset  : BorderStyle
 235 |     Outset : BorderStyle
 236 | 
 237 | 
 238 |   export
 239 |   Interpolation BorderStyle where
 240 |     interpolate None   = "none"
 241 |     interpolate Hidden = "hidden"
 242 |     interpolate Dotted = "dotted"
 243 |     interpolate Dashed = "dashed"
 244 |     interpolate Solid  = "solid"
 245 |     interpolate Dbl    = "double"
 246 |     interpolate Groove = "groove"
 247 |     interpolate Ridge  = "ridge"
 248 |     interpolate Inset  = "inset"
 249 |     interpolate Outset = "outset"
 250 | 
 251 | namespace BorderWidth
 252 |   public export
 253 |   data BorderWidth : Type where
 254 |     BL     : Length -> BorderWidth
 255 |     Thin   : BorderWidth
 256 |     Medium : BorderWidth
 257 |     Thick  : BorderWidth
 258 | 
 259 |   export
 260 |   Interpolation BorderWidth where
 261 |     interpolate (BL x) = interpolate x
 262 |     interpolate Thin   = "thin"
 263 |     interpolate Medium = "medium"
 264 |     interpolate Thick  = "thick"
 265 | 
 266 |   export %inline
 267 |   Cast Length BorderWidth where
 268 |     cast = BL
 269 | 
 270 | namespace Linecap
 271 |   public export
 272 |   data Linecap : Type where
 273 |     Butt   : Linecap
 274 |     Round  : Linecap
 275 |     Square : Linecap
 276 | 
 277 |   export
 278 |   Interpolation Linecap where
 279 |     interpolate Butt   = "butt"
 280 |     interpolate Round  = "round"
 281 |     interpolate Square = "square"
 282 | 
 283 | namespace Linejoin
 284 |   public export
 285 |   data Linejoin : Type where
 286 |     Bevel : Linejoin
 287 |     Miter : Linejoin
 288 |     Round : Linejoin
 289 | 
 290 |   export
 291 |   Interpolation Linejoin where
 292 |     interpolate Bevel = "bevel"
 293 |     interpolate Miter = "miter"
 294 |     interpolate Round = "round"
 295 | 
 296 | namespace LineHeight
 297 |   public export
 298 |   data LineHeight : Type where
 299 |     Normal : LineHeight
 300 |     LHD    : Double -> LineHeight
 301 |     LHL    : Length -> LineHeight
 302 |     LHP    : Percentage -> LineHeight
 303 | 
 304 |   export
 305 |   Interpolation LineHeight where
 306 |     interpolate Normal  = "normal"
 307 |     interpolate (LHD x) = show x
 308 |     interpolate (LHL x) = interpolate x
 309 |     interpolate (LHP x) = interpolate x
 310 | 
 311 |   export %inline
 312 |   Cast Length LineHeight where
 313 |     cast = LHL
 314 | 
 315 |   export %inline
 316 |   Cast Percentage LineHeight where
 317 |     cast = LHP
 318 | 
 319 |   export %inline
 320 |   fromInteger : Integer -> LineHeight
 321 |   fromInteger = LHD . cast
 322 | 
 323 |   export %inline
 324 |   FromDouble LineHeight where
 325 |     fromDouble = LHD
 326 | 
 327 | namespace Overflow
 328 | 
 329 |   ||| The `overflow-x` and `overflow-y` CSS properties set
 330 |   ||| what shows when content overflows a block-level element's
 331 |   ||| edges. This may be nothing, a scroll bar,
 332 |   ||| or the overflow content.
 333 |   public export
 334 |   data Overflow : Type where
 335 | 
 336 |     ||| Content is not clipped and may be rendered outside the padding box's edges.
 337 |     Visible : Overflow
 338 | 
 339 |     ||| Content is clipped if necessary to fit horizontally
 340 |     ||| in the padding box. No scrollbars are provided.
 341 |     ||| Programmatic scrolling is still possible.
 342 |     Hidden  : Overflow
 343 | 
 344 |     ||| Like `Hidden` but forbidding also programmatic scrolling.
 345 |     Clip    : Overflow
 346 | 
 347 |     ||| Content is clipped if necessary to fit in the padding box.
 348 |     ||| Browsers display scrollbars whether or not any content is actually clipped.
 349 |     ||| (This prevents scrollbars from appearing or disappearing when the
 350 |     ||| content changes.)
 351 |     Scroll  : Overflow
 352 | 
 353 |     ||| Depends on the user agent. If content fits inside the
 354 |     ||| padding box, it looks the same as visible, but still
 355 |     ||| establishes a new block-formatting context. Desktop browsers
 356 |     ||| provide scrollbars if content overflows.
 357 |     Auto    : Overflow
 358 | 
 359 |   export
 360 |   Interpolation Overflow where
 361 |     interpolate Visible = "visible"
 362 |     interpolate Hidden  = "hidden"
 363 |     interpolate Clip    = "clip"
 364 |     interpolate Scroll  = "scroll"
 365 |     interpolate Auto    = "auto"
 366 | 
 367 | namespace Pos
 368 |   public export
 369 |   data Pos : Type where
 370 |     PL       : Length -> Pos
 371 |     PP       : Percentage -> Pos
 372 | 
 373 |   export
 374 |   Interpolation Pos where
 375 |     interpolate (PL x)   = interpolate x
 376 |     interpolate (PP x)   = interpolate x
 377 | 
 378 |   export %inline
 379 |   Cast Length Pos where
 380 |     cast = PL
 381 | 
 382 |   export %inline
 383 |   Cast Percentage Pos where
 384 |     cast = PP
 385 | 
 386 | namespace Position
 387 |   public export
 388 |   data Position = Static | Relative | Absolute | Fixed | Sticky
 389 | 
 390 |   export
 391 |   Interpolation Position where
 392 |     interpolate Static   = "static"
 393 |     interpolate Relative = "relative"
 394 |     interpolate Absolute = "absolute"
 395 |     interpolate Fixed    = "fixed"
 396 |     interpolate Sticky   = "sticky"
 397 | 
 398 | namespace Ratio
 399 |   public export
 400 |   data Ratio : Type where
 401 |     Auto : Ratio
 402 |     RD   : Double -> Ratio
 403 |     RDD  : Double -> Double -> Ratio
 404 | 
 405 |   export
 406 |   Interpolation Ratio where
 407 |     interpolate Auto      = "auto"
 408 |     interpolate (RD x)    = show x
 409 |     interpolate (RDD x y) = "\{show x}/\{show y}"
 410 | 
 411 |   export %inline
 412 |   fromInteger : Integer -> Ratio
 413 |   fromInteger = RD . cast
 414 | 
 415 |   export %inline
 416 |   FromDouble Ratio where
 417 |     fromDouble = RD
 418 | 
 419 | namespace Resize
 420 |   public export
 421 |   data Resize = None | Vertical | Horizontal | Both
 422 | 
 423 |   export
 424 |   Interpolation Resize where
 425 |     interpolate None       = "none"
 426 |     interpolate Vertical   = "vertical"
 427 |     interpolate Horizontal = "horizontal"
 428 |     interpolate Both       = "both"
 429 | 
 430 | namespace ScrollbarGutter
 431 |   public export
 432 |   data ScrollbarGutter = Auto | Stable | BothEdges
 433 | 
 434 |   export
 435 |   Interpolation ScrollbarGutter where
 436 |     interpolate Auto      = "auto"
 437 |     interpolate Stable    = "stable"
 438 |     interpolate BothEdges = "stable both-edges"
 439 | 
 440 | namespace TextAlign
 441 |   public export
 442 |   data TextAlign : Type where
 443 |     ||| The same as left if direction is left-to-right and right if direction is right-to-left.
 444 |     Start   : TextAlign
 445 |     ||| The same as right if direction is left-to-right and left if direction is right-to-left.
 446 |     End     : TextAlign
 447 |     ||| The inline contents are aligned to the left edge of the line box.
 448 |     Left    : TextAlign
 449 |     ||| The inline contents are aligned to the right edge of the line box.
 450 |     Right   : TextAlign
 451 |     ||| The inline contents are centered within the line box.
 452 |     Center  : TextAlign
 453 |     ||| 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.
 454 |     Justify : TextAlign
 455 | 
 456 |   export
 457 |   Interpolation TextAlign where
 458 |     interpolate Start   = "start"
 459 |     interpolate End     = "end"
 460 |     interpolate Left    = "left"
 461 |     interpolate Right   = "right"
 462 |     interpolate Center  = "center"
 463 |     interpolate Justify = "justify"
 464 | 
 465 | namespace TextDecorationLine
 466 | 
 467 |   public export
 468 |   data TextDecorationLine : Type where
 469 |     None        : TextDecorationLine
 470 |     Underline   : TextDecorationLine
 471 |     Overline    : TextDecorationLine
 472 |     LineThrough : TextDecorationLine
 473 | 
 474 |   export
 475 |   Interpolation TextDecorationLine where
 476 |     interpolate None        = "none"
 477 |     interpolate Underline   = "underline"
 478 |     interpolate Overline    = "overline"
 479 |     interpolate LineThrough = "line-through"
 480 | 
 481 | namespace TextDecorationStyle
 482 | 
 483 |   public export
 484 |   data TextDecorationStyle : Type where
 485 |     Solid  : TextDecorationStyle
 486 |     Dbl    : TextDecorationStyle
 487 |     Dotted : TextDecorationStyle
 488 |     Dashed : TextDecorationStyle
 489 |     Wavy   : TextDecorationStyle
 490 | 
 491 |   export
 492 |   Interpolation TextDecorationStyle where
 493 |     interpolate Solid  = "solid"
 494 |     interpolate Dbl    = "double"
 495 |     interpolate Dotted = "dotted"
 496 |     interpolate Dashed = "dashed"
 497 |     interpolate Wavy   = "wavy"
 498 | 
 499 | namespace TextOverflow
 500 |   public export
 501 |   data TextOverflow = Clip | Ellipsis
 502 | 
 503 |   export
 504 |   Interpolation TextOverflow where
 505 |     interpolate Clip     = "clip"
 506 |     interpolate Ellipsis = "ellipsis"
 507 | 
 508 | namespace Width
 509 |   public export
 510 |   data Width : Type where
 511 |     WL       : Length -> Width
 512 |     WP       : Percentage -> Width
 513 | 
 514 |   export
 515 |   Interpolation Width where
 516 |     interpolate (WL x)   = interpolate x
 517 |     interpolate (WP x)   = interpolate x
 518 | 
 519 |   export %inline
 520 |   Cast Length Width where
 521 |     cast = WL
 522 | 
 523 |   export %inline
 524 |   Cast Percentage Width where
 525 |     cast = WP
 526 | 
 527 | namespace Visibility
 528 | 
 529 |   public export
 530 |   data Visibility = Visible | Hidden | Collapse
 531 | 
 532 |   export
 533 |   Interpolation Visibility where
 534 |     interpolate Visible  = "visible"
 535 |     interpolate Hidden   = "hidden"
 536 |     interpolate Collapse = "collapse"
 537 | 
 538 | namespace WiteSpace
 539 | 
 540 |   ||| Handles white space inside an element
 541 |   public export
 542 |   data WhiteSpace : Type where
 543 |     ||| White space is collapsed (several white space characters
 544 |     ||| are treated as a single space character) and lines are
 545 |     ||| broken as necessary.
 546 |     Normal      : WhiteSpace
 547 | 
 548 |     ||| Like `Normal` but suppresses line breaks (text wrapping)
 549 |     Nowrap      : WhiteSpace
 550 | 
 551 |     ||| Sequences of white space are preserved. Lines are broken at
 552 |     ||| newline characters and at `<br>` elements.
 553 |     Pre         : WhiteSpace
 554 | 
 555 |     ||| Sequences of white space are preserved. Lines are broken at
 556 |     ||| newline characters, at `<br>` elements, and as necessary
 557 |     ||| to fill the box.
 558 |     PreWrap     : WhiteSpace
 559 | 
 560 |     ||| Like `PreWrap` but collapses sequences of white space.
 561 |     PreLine     : WhiteSpace
 562 | 
 563 |     ||| The behavior is identical to that of `PreWrap`, except that:
 564 |     |||
 565 |     ||| * Any sequence of preserved white space always takes up space,
 566 |     |||   including at the end of the line.
 567 |     ||| * A line breaking opportunity exists after every preserved
 568 |     |||   white space character, including between white space characters.
 569 |     ||| * Such preserved spaces take up space and do not hang,
 570 |     |||   and thus affect the box's intrinsic sizes
 571 |     |||   (min-content size and max-content size).
 572 |     BreakSpaces : WhiteSpace
 573 | 
 574 |   export
 575 |   Interpolation WhiteSpace where
 576 |     interpolate Normal      = "normal"
 577 |     interpolate Nowrap      = "nowrap"
 578 |     interpolate Pre         = "pre"
 579 |     interpolate PreWrap     = "pre-wrap"
 580 |     interpolate PreLine     = "pre-line"
 581 |     interpolate BreakSpaces = "break-spaces"
 582 |