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