0 | module Text.HTML.DomID
  1 |
  2 | import Data.List.Quantifiers
  3 | import Derive.Prelude
  4 | import Text.HTML
  5 |
  6 | %default total
  7 | %language ElabReflection
  8 |
  9 | ||| Utility data type for accessing elements in the DOM.
 10 | |||
 11 | ||| This will improve type safety and give clearer semantics to a string
 12 | ||| that is to be used as an identifier in the DOM.
 13 | public export
 14 | record DomID where
 15 |   constructor D
 16 |   value : String
 17 |
 18 | %runElab derive "DomID" [Show,Eq,Ord,FromString]
 19 |
 20 | ||| Alias for `cast` with better type inference.
 21 | export %inline
 22 | toID : Cast t DomID => t -> DomID
 23 | toID = cast
 24 |
 25 | ||| Specialized version of `withId` (which sets the `id` attribute of a
 26 | ||| node) for working with `DomID`s.
 27 | export %inline
 28 | withDomID : Cast t DomID => t -> Node e -> Node e
 29 | withDomID = withId . value . toID
 30 |
 31 | ||| Set the `for` attribute of a DOM label to the given ID.
 32 | export %inline
 33 | forID : Cast t DomID => t -> Attribute x e
 34 | forID = for . value . toID
 35 |
 36 | --------------------------------------------------------------------------------
 37 | -- Implementations
 38 | --------------------------------------------------------------------------------
 39 |
 40 | export
 41 | Interpolation DomID where interpolate = value
 42 |
 43 | export
 44 | Semigroup DomID where
 45 |   D x <+> D y = D $ x ++ "-" ++ y
 46 |
 47 | export %inline
 48 | Cast Nat DomID where cast = D . show
 49 |
 50 | export
 51 | Cast x DomID => Cast (SnocList x) DomID where
 52 |   cast [<]       = D "lin"
 53 |   cast (sx :< x) = cast sx <+> cast x
 54 |
 55 | export
 56 | Cast x DomID => Cast (List x) DomID where
 57 |   cast []      = D "nil"
 58 |   cast (x::xs) = cast x <+> cast xs
 59 |
 60 | export
 61 | (prf : All (\x => Cast (f x) DomID) ks) => Cast (List.Quantifiers.All.All f ks) DomID where
 62 |   cast []              = "nil"
 63 |   cast @{_::_} (x::xs) = cast x <+> cast xs
 64 |
 65 | --------------------------------------------------------------------------------
 66 | -- Accessing DOM Elements
 67 | --------------------------------------------------------------------------------
 68 |
 69 | export %inline
 70 | tagRef : {s : _} -> (0 tag : HTMLTag s) -> Cast t DomID => t -> Ref tag
 71 | tagRef _ v = Id (value $ cast v)
 72 |
 73 | export %inline
 74 | elemRef : Cast t DomID => t -> Ref Void
 75 | elemRef v = Elem (value $ cast v)
 76 |
 77 | ||| Identifier for accessing a `<button>` element
 78 | export %inline
 79 | btnRef : Cast t DomID => t -> Ref Tag.Button
 80 | btnRef = tagRef _
 81 |
 82 | ||| Identifier for accessing a `<div>` element
 83 | export %inline
 84 | divRef : Cast t DomID => t -> Ref Tag.Div
 85 | divRef = tagRef _
 86 |
 87 | ||| Identifier for accessing an `<input>` element
 88 | export %inline
 89 | inpRef : Cast t DomID => t -> Ref Tag.Input
 90 | inpRef = tagRef _
 91 |
 92 | ||| Identifier for accessing a `<canvas>` element
 93 | export %inline
 94 | canvasRef : Cast t DomID => t -> Ref Tag.Canvas
 95 | canvasRef = tagRef _
 96 |
 97 | ||| `id` attribute for a DOM element
 98 | export %inline
 99 | ref : {s : _} -> {0 tag : HTMLTag s} -> Cast t DomID => t -> Attribute tag e
100 | ref = Id . tagRef tag
101 |