0 | module Text.HTML.Ref
 1 |
 2 | import Text.HTML.Tag
 3 |
 4 | %default total
 5 |
 6 | ||| A typed reference to an element or container in the DOM. Elements can
 7 | |||
 8 | ||| This can be used as a type-safe ID when constructing
 9 | ||| HTML nodes and their attribute lists.
10 | ||| In addition, we provide (pseudo-)element references for
11 | ||| `body`, `document`, and `window`.
12 | public export
13 | data Ref : {0 k : Type} -> (t : k) -> Type where
14 |   Id :  {tag   : String}
15 |      -> {0 tpe : HTMLTag tag}
16 |      -> (id    : String)
17 |      -> Ref tpe
18 |
19 |   Elem     : String -> Ref Void
20 |
21 |   Body     : Ref Void
22 |
23 |   Document : Ref Void
24 |
25 |   Window   : Ref Void
26 |