
   0 | module Text.HTML.Attribute
   1 | 
   2 | import Derive.Prelude
   3 | import Data.Linear.Token
   4 | import Data.List
   5 | import Data.Maybe
   6 | import Data.String
   7 | import FS.Concurrent.Signal
   8 | import Text.CSS.Class
   9 | import Text.CSS.Declaration
  10 | import Text.HTML.Event
  11 | import Text.HTML.Ref
  12 | import Text.HTML.Tag
  13 | 
  14 | %default total
  15 | %language ElabReflection
  16 | 
  17 | --------------------------------------------------------------------------------
  18 | -- Attribute
  19 | --------------------------------------------------------------------------------
  20 | 
  21 | public export
  22 | data Dir = LTR | RTL
  23 | 
  24 | export
  25 | Show Dir where
  26 |   show LTR = "ltr"
  27 |   show RTL = "rtl"
  28 | 
  29 | public export
  30 | data LoadType = Lzy | Eager
  31 | 
  32 | export
  33 | Show LoadType where
  34 |   show Lzy   = "lazy"
  35 |   show Eager = "eager"
  36 | 
  37 | ||| Enum representing different types of input elements
  38 | public export
  39 | data InputType =
  40 |     Button
  41 |   | CheckBox
  42 |   | Color
  43 |   | Date
  44 |   | DateTime
  45 |   | Email
  46 |   | File
  47 |   | Image
  48 |   | Month
  49 |   | Number
  50 |   | Password
  51 |   | Radio
  52 |   | Range
  53 |   | Tel
  54 |   | Text
  55 |   | Time
  56 |   | URL
  57 |   | Week
  58 | 
  59 | export
  60 | Show InputType where
  61 |   show Button   = "button"
  62 |   show CheckBox = "checkbox"
  63 |   show Color    = "color"
  64 |   show Date     = "date"
  65 |   show DateTime = "datetime-local"
  66 |   show Email    = "email"
  67 |   show File     = "file"
  68 |   show Image    = "image"
  69 |   show Month    = "month"
  70 |   show Number   = "number"
  71 |   show Password = "password"
  72 |   show Radio    = "radio"
  73 |   show Range    = "range"
  74 |   show Tel      = "tel"
  75 |   show Text     = "text"
  76 |   show Time     = "time"
  77 |   show URL      = "url"
  78 |   show Week     = "week"
  79 | 
  80 | ||| An attribute indexed by the `HTMLTag` used for the element
  81 | ||| in question.
  82 | |||
  83 | ||| This allows us to make sure we don't use invalid `Ref`s (which can
  84 | ||| be later used to retrieve an element from the DOM) in a HTML node.
  85 | public export
  86 | data Attribute : {0 k : Type} -> (t : k) -> Type where
  87 |   Id     : {0 t : HTMLTag s} -> Ref t -> Attribute t
  88 |   Str    : (name : String) -> (value : String) -> Attribute t
  89 |   Bool   : (name : String) -> (value : Bool) -> Attribute t
  90 |   Event_ :
  91 |        {0 event : Type}
  92 |     -> (preventDefault, stopPropagation : Bool)
  93 |     -> {auto sink : Sink event}
  94 |     -> DOMEvent event
  95 |     -> Attribute t
  96 |   Empty  : Attribute t
  97 | 
  98 | ||| Tries to extract the ID from a list of attributes
  99 | export
 100 | attrID : List (Attribute t) -> Maybe (Ref t)
 101 | attrID []           = Nothing
 102 | attrID (Id r :: _)  = Just r
 103 | attrID (_    :: xs) = attrID xs
 104 | 
 105 | ||| Optional attribute that is set to `Empty` if the given `Bool` is `False`
 106 | export
 107 | attrIf : Bool -> Lazy (Attribute t) -> Attribute t
 108 | attrIf True n  = n
 109 | attrIf False _ = Empty
 110 | 
 111 | public export
 112 | Attributes : {0 k : _} -> (t : k) -> Type
 113 | Attributes t = List (Attribute t)
 114 | 
 115 | export %inline
 116 | Event : Sink ev => DOMEvent ev -> Attribute t
 117 | Event = Event_ False False
 118 | 
 119 | export
 120 | displayAttribute : Attribute t -> Maybe String
 121 | displayAttribute (Id (Id va))   = Just #"id="\#{va}""#
 122 | displayAttribute (Str nm va)    = Just #"\#{nm}="\#{va}""#
 123 | displayAttribute (Bool nm True) = Just nm
 124 | displayAttribute (Bool _ False) = Nothing
 125 | displayAttribute (Event_ _ _ _) = Nothing
 126 | displayAttribute Empty          = Nothing
 127 | 
 128 | export
 129 | displayAttributes : Attributes t -> String
 130 | displayAttributes = fastConcat . intersperse " " . mapMaybe displayAttribute
 131 | 
 132 | export
 133 | dispAttr : String -> (a -> String) -> a -> Attribute t
 134 | dispAttr nm f =  Str nm . f
 135 | 
 136 | export
 137 | showAttr : Show a => String -> a -> Attribute t
 138 | showAttr nm = dispAttr nm show
 139 | 
 140 | export %inline
 141 | accept : String -> Attribute t
 142 | accept = Str "accept"
 143 | 
 144 | export
 145 | acceptAll : List String -> Attribute t
 146 | acceptAll = accept . fastConcat . intersperse ","
 147 | 
 148 | export %inline
 149 | accesskey : String -> Attribute t
 150 | accesskey = Str "accesskey"
 151 | 
 152 | export %inline
 153 | action : String -> Attribute t
 154 | action = Str "action"
 155 | 
 156 | export %inline
 157 | alt : String -> Attribute t
 158 | alt = Str "alt"
 159 | 
 160 | export %inline
 161 | autocapitalize : Bool -> Attribute t
 162 | autocapitalize = Bool "autocapitalize"
 163 | 
 164 | export %inline
 165 | autocomplete : Bool -> Attribute t
 166 | autocomplete = Bool "autocomplete"
 167 | 
 168 | export %inline
 169 | autofocus : Bool -> Attribute t
 170 | autofocus = Bool "autofocus"
 171 | 
 172 | export %inline
 173 | autoplay : Bool -> Attribute t
 174 | autoplay = Bool "autoplay"
 175 | 
 176 | export %inline
 177 | checked : Bool -> Attribute t
 178 | checked = Bool "checked"
 179 | 
 180 | export %inline
 181 | cite : String -> Attribute t
 182 | cite = Str "cite"
 183 | 
 184 | export %inline
 185 | class : Class -> Attribute t
 186 | class = Str "class" . value
 187 | 
 188 | export %inline
 189 | classes : Classes -> Attribute t
 190 | classes = dispAttr "class" (fastConcat . intersperse " " . map value)
 191 | 
 192 | export %inline
 193 | cols : Bits32 -> Attribute t
 194 | cols = showAttr "cols"
 195 | 
 196 | export %inline
 197 | colspan : Bits32 -> Attribute t
 198 | colspan = showAttr "colspan"
 199 | 
 200 | export %inline
 201 | contenteditable : Bool -> Attribute t
 202 | contenteditable = Bool "contenteditable"
 203 | 
 204 | export %inline
 205 | controls : Bool -> Attribute t
 206 | controls = Bool "controls"
 207 | 
 208 | export %inline
 209 | data_ : String -> Attribute t
 210 | data_ = Str "data"
 211 | 
 212 | export %inline
 213 | dir : Dir -> Attribute t
 214 | dir = showAttr "dir"
 215 | 
 216 | export %inline
 217 | disabled : Bool -> Attribute t
 218 | disabled = Bool "disabled"
 219 | 
 220 | export %inline
 221 | download : String -> Attribute t
 222 | download = Str "download"
 223 | 
 224 | export %inline
 225 | draggable : Bool -> Attribute t
 226 | draggable = Bool "draggable"
 227 | 
 228 | export %inline
 229 | for : String -> Attribute t
 230 | for = Str "for"
 231 | 
 232 | export %inline
 233 | form : String -> Attribute t
 234 | form = Str "form"
 235 | 
 236 | export %inline
 237 | height : Bits32 -> Attribute t
 238 | height = showAttr "height"
 239 | 
 240 | export %inline
 241 | hidden : Bool -> Attribute t
 242 | hidden = Bool "hidden"
 243 | 
 244 | export %inline
 245 | href : String -> Attribute t
 246 | href = Str "href"
 247 | 
 248 | export %inline
 249 | hreflang : String -> Attribute t
 250 | hreflang = Str "hreflang"
 251 | 
 252 | export %inline
 253 | id : String -> Attribute t
 254 | id = Str "id"
 255 | 
 256 | export %inline
 257 | label : String -> Attribute t
 258 | label = Str "label"
 259 | 
 260 | export %inline
 261 | lang : String -> Attribute t
 262 | lang = Str "lang"
 263 | 
 264 | export %inline
 265 | loading : LoadType -> Attribute t
 266 | loading = showAttr "loading"
 267 | 
 268 | export %inline
 269 | list : String -> Attribute t
 270 | list = Str "list"
 271 | 
 272 | export %inline
 273 | loop : Bool -> Attribute t
 274 | loop = Bool "loop"
 275 | 
 276 | export %inline
 277 | maxlength : Bits32 -> Attribute t
 278 | maxlength = showAttr "maxlength"
 279 | 
 280 | export %inline
 281 | minlength : Bits32 -> Attribute t
 282 | minlength = showAttr "minlength"
 283 | 
 284 | export %inline
 285 | multiple : Bool -> Attribute t
 286 | multiple = Bool "multiple"
 287 | 
 288 | export %inline
 289 | muted : Bool -> Attribute t
 290 | muted = Bool "muted"
 291 | 
 292 | export %inline
 293 | name : String -> Attribute t
 294 | name = Str "name"
 295 | 
 296 | export %inline
 297 | placeholder : String -> Attribute t
 298 | placeholder = Str "placeholder"
 299 | 
 300 | export %inline
 301 | readonly : Bool -> Attribute t
 302 | readonly = Bool "readonly"
 303 | 
 304 | export %inline
 305 | required : Bool -> Attribute t
 306 | required = Bool "required"
 307 | 
 308 | export %inline
 309 | reverse : Bool -> Attribute t
 310 | reverse = Bool "reverse"
 311 | 
 312 | export %inline
 313 | rows : Bits32 -> Attribute t
 314 | rows = showAttr "rows"
 315 | 
 316 | export %inline
 317 | rowspan : Bits32 -> Attribute t
 318 | rowspan = showAttr "rowspan"
 319 | 
 320 | export %inline
 321 | selected : Bool -> Attribute t
 322 | selected = Bool "selected"
 323 | 
 324 | export %inline
 325 | spellcheck : Bool -> Attribute t
 326 | spellcheck = Bool "spellcheck"
 327 | 
 328 | export %inline
 329 | src : String -> Attribute t
 330 | src = Str "src"
 331 | 
 332 | export
 333 | style : List Declaration -> Attribute t
 334 | style = Str "style" . fastConcat . map interpolate
 335 | 
 336 | export %inline
 337 | tabindex : Int32 -> Attribute t
 338 | tabindex = showAttr "tabindex"
 339 | 
 340 | export %inline
 341 | target : String -> Attribute t
 342 | target = Str "target"
 343 | 
 344 | export %inline
 345 | title : String -> Attribute t
 346 | title = Str "title"
 347 | 
 348 | export %inline
 349 | type : InputType -> Attribute t
 350 | type = showAttr "type"
 351 | 
 352 | export %inline
 353 | value : String -> Attribute t
 354 | value = Str "value"
 355 | 
 356 | export %inline
 357 | width : Bits32 -> Attribute t
 358 | width = showAttr "width"
 359 | 
 360 | export %inline
 361 | wrap : Bool -> Attribute t
 362 | wrap = Bool "wrap"
 363 | 
 364 | --------------------------------------------------------------------------------
 365 | --          Events
 366 | --------------------------------------------------------------------------------
 367 | 
 368 | parameters {auto sink : Sink ev}
 369 | 
 370 |   export %inline
 371 |   click : (MouseInfo -> Maybe ev) -> Attribute t
 372 |   click = Event . Click
 373 | 
 374 |   export %inline
 375 |   mouseDown : (MouseInfo -> Maybe ev) -> Attribute t
 376 |   mouseDown = Event . MouseDown
 377 | 
 378 |   export %inline
 379 |   mouseUp : (MouseInfo -> Maybe ev) -> Attribute t
 380 |   mouseUp = Event . MouseUp
 381 | 
 382 |   export %inline
 383 |   mouseMove : (MouseInfo -> Maybe ev) -> Attribute t
 384 |   mouseMove = Event . MouseMove
 385 | 
 386 |   export
 387 |   leftDown : (MouseInfo -> Maybe ev) -> Attribute t
 388 |   leftDown f = mouseDown (\mi => guard (mi.button == 0) >> f mi)
 389 | 
 390 |   export
 391 |   leftUp : (MouseInfo -> Maybe ev) -> Attribute t
 392 |   leftUp f = mouseUp (\mi => guard (mi.button == 0) >> f mi)
 393 | 
 394 |   export
 395 |   rightDown : (MouseInfo -> Maybe ev) -> Attribute t
 396 |   rightDown f = mouseDown (\mi => guard (mi.button == 2) >> f mi)
 397 | 
 398 |   export
 399 |   rightUp : (MouseInfo -> Maybe ev) -> Attribute t
 400 |   rightUp f = mouseUp (\mi => guard (mi.button == 2) >> f mi)
 401 | 
 402 |   export
 403 |   middleDown : (MouseInfo -> Maybe ev) -> Attribute t
 404 |   middleDown f = mouseDown (\mi => guard (mi.button == 1) >> f mi)
 405 | 
 406 |   export
 407 |   middleUp : (MouseInfo -> Maybe ev) -> Attribute t
 408 |   middleUp f = mouseUp (\mi => guard (mi.button == 1) >> f mi)
 409 | 
 410 |   export %inline
 411 |   onLeftDown : ev -> Attribute t
 412 |   onLeftDown = leftDown . const . Just
 413 | 
 414 |   export %inline
 415 |   onLeftUp : ev -> Attribute t
 416 |   onLeftUp = leftUp . const . Just
 417 | 
 418 |   export %inline
 419 |   onRightDown : ev -> Attribute t
 420 |   onRightDown = rightDown . const . Just
 421 | 
 422 |   export %inline
 423 |   onRightUp : ev -> Attribute t
 424 |   onRightUp = rightUp . const . Just
 425 | 
 426 |   export %inline
 427 |   onMiddleDown : ev -> Attribute t
 428 |   onMiddleDown = middleDown . const . Just
 429 | 
 430 |   export %inline
 431 |   onMiddleUp : ev -> Attribute t
 432 |   onMiddleUp = middleUp . const . Just
 433 | 
 434 |   export %inline
 435 |   onClick : ev -> Attribute t
 436 |   onClick = click . const . Just
 437 | 
 438 |   export
 439 |   onLeftClick : ev -> Attribute t
 440 |   onLeftClick va = click $ \mi => toMaybe (mi.button == 0) va
 441 | 
 442 |   export
 443 |   onRightClick : ev -> Attribute t
 444 |   onRightClick va = click $ \mi => toMaybe (mi.button == 2) va
 445 | 
 446 |   export
 447 |   onMiddleClick : ev -> Attribute t
 448 |   onMiddleClick va = click $ \mi => toMaybe (mi.button == 1) va
 449 | 
 450 |   export %inline
 451 |   dblClick : (MouseInfo -> Maybe ev) -> Attribute t
 452 |   dblClick = Event . DblClick
 453 | 
 454 |   export %inline
 455 |   onDblClick : ev -> Attribute t
 456 |   onDblClick = dblClick . const . Just
 457 | 
 458 |   export %inline
 459 |   onMouseEnter : ev -> Attribute t
 460 |   onMouseEnter = Event . MouseEnter . const . Just
 461 | 
 462 |   export %inline
 463 |   onMouseLeave : ev -> Attribute t
 464 |   onMouseLeave = Event . MouseLeave . const . Just
 465 | 
 466 |   export %inline
 467 |   onMouseOver : ev -> Attribute t
 468 |   onMouseOver = Event . MouseOver . const . Just
 469 | 
 470 |   export %inline
 471 |   onMouseOut : ev -> Attribute t
 472 |   onMouseOut = Event . MouseOut . const . Just
 473 | 
 474 |   export
 475 |   onResize : (Rect -> ev) -> Attribute t
 476 |   onResize f = Event . Resize $ Just . f
 477 | 
 478 |   export
 479 |   onChange : (String -> ev) -> Attribute t
 480 |   onChange f = Event . Change $ Just . f . value
 481 | 
 482 |   export
 483 |   onChangeMaybe : (String -> Maybe ev) -> Attribute t
 484 |   onChangeMaybe f = Event . Change $ f . value
 485 | 
 486 |   export
 487 |   onChecked : (Bool -> ev) -> Attribute t
 488 |   onChecked f = Event . Change $ Just . f . checked
 489 | 
 490 |   export
 491 |   onInput : (String -> ev) -> Attribute t
 492 |   onInput f = Event . Input $ Just . f . value
 493 | 
 494 |   export
 495 |   onScroll : (ScrollInfo -> ev) -> Attribute t
 496 |   onScroll f = Event . Scroll $ Just . f
 497 | 
 498 |   export
 499 |   onEnterDown : ev -> Attribute t
 500 |   onEnterDown va = Event . KeyDown $ \k => toMaybe (k.key == "Enter") va
 501 | 
 502 |   export
 503 |   onEscDown : ev -> Attribute t
 504 |   onEscDown va = Event . KeyDown $ \k => toMaybe (k.key == "Escape") va
 505 | 
 506 |   export
 507 |   onKeyUp : (KeyInfo -> ev) -> Attribute t
 508 |   onKeyUp f = Event . KeyUp $ Just . f
 509 | 
 510 |   export
 511 |   onBlur : ev -> Attribute t
 512 |   onBlur = Event . Blur
 513 | 
 514 |   export
 515 |   onFocus : ev -> Attribute t
 516 |   onFocus = Event . Focus
 517 | 
 518 |   export
 519 |   onRemove : ev -> Attribute t
 520 |   onRemove = Event . Remove
 521 | 
 522 |   export
 523 |   onClose : ev -> Attribute t
 524 |   onClose = Event . Close
 525 |