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