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