0 | module Rhone.JS.ElemRef
  1 |
  2 | import JS
  3 | import Text.CSS
  4 | import Text.Html
  5 | import Web.Dom
  6 |
  7 | %default total
  8 |
  9 | --------------------------------------------------------------------------------
 10 | --          ElemRef
 11 | --------------------------------------------------------------------------------
 12 |
 13 | ||| A typed reference to an element or container in the DOM. Elements can
 14 | ||| either be referenced by their ID string or their CSS class
 15 | ||| (both of which must be unique), or by holding a value directly.
 16 | ||| This can be used to access the element in question,
 17 | ||| for instance by invoking `getElementByRef`.
 18 | |||
 19 | ||| In addition, we provide (pseudo-)element references for
 20 | ||| `body`, `document`, and `window`.
 21 | public export
 22 | data ElemRef : (t : Type) -> Type where
 23 |   Id :  {tag   : String}
 24 |      -> (0 tpe : ElementType tag t)
 25 |      -> (id    : String)
 26 |      -> ElemRef t
 27 |
 28 |   Class :  {tag   : String}
 29 |         -> (0 tpe : ElementType tag t)
 30 |         -> (class : String)
 31 |         -> ElemRef t
 32 |
 33 |   Body : ElemRef HTMLElement
 34 |
 35 |   Document : ElemRef Document
 36 |
 37 |   Window : ElemRef Window
 38 |
 39 | ||| Predicate witnessing that a given `ElemRef` is a reference
 40 | ||| by ID.
 41 | public export
 42 | data ById : ElemRef t -> Type where
 43 |   IsById : {0 tpe : _} -> {0 id : _} -> ById (Id tpe id)
 44 |
 45 | ||| Predicate witnessing that a given `ElemRef` is a reference
 46 | ||| by Class.
 47 | public export
 48 | data ByClass : ElemRef t -> Type where
 49 |   IsByClass : {0 tpe : _} -> {0 id : _} -> ByClass (Class tpe id)
 50 |
 51 | namespace Attribute
 52 |   ||| Uses an element ref as an ID attribute
 53 |   export
 54 |   ref : (r : ElemRef t) -> {auto 0 _ : ById r} -> Attribute ev
 55 |   ref (Id _ i) = id i
 56 |
 57 | namespace CSS
 58 |   ||| Uses an element ref as an ID selector
 59 |   export
 60 |   idRef : (r : ElemRef t) -> {auto 0 _ : ById r} -> List Declaration -> Rule n
 61 |   idRef (Id _ i) = id i
 62 |
 63 |   ||| Uses an element ref as a class selector
 64 |   export
 65 |   classRef : (r : ElemRef t) -> {auto 0 _ : ByClass r} -> List Declaration -> Rule n
 66 |   classRef (Class _ i) = class i
 67 |
 68 | --------------------------------------------------------------------------------
 69 | --          Inserting Nodes
 70 | --------------------------------------------------------------------------------
 71 |
 72 | ||| Tries to retrieve an element of the given type by looking
 73 | ||| up its ID in the DOM. Unlike `getElementById`, this will throw
 74 | ||| an exception in the `JSIO` monad if the element is not found
 75 | ||| or can't be safely cast to the desired type.
 76 | export
 77 | strictGetElementById : SafeCast t => (tag,id : String) -> JSIO t
 78 | strictGetElementById tag id = do
 79 |   Nothing <- castElementById t id | Just t => pure t
 80 |   liftJSIO $ throwError $
 81 |     Caught "Control.Monad.Dom.Interface.strictGetElementById: Could not find \{tag} with id \{id}"
 82 |
 83 | ||| Tries to retrieve a HTMLElement by looking
 84 | ||| up its ID in the DOM. Unlike `getElementById`, this will throw
 85 | ||| an exception in the `JSIO` monad if the element is not found
 86 | ||| or can't be safely cast to the desired type.
 87 | export %inline
 88 | strictGetHTMLElementById : (tag,id : String) -> JSIO HTMLElement
 89 | strictGetHTMLElementById = strictGetElementById
 90 |
 91 | ||| Tries to retrieve an element of the given type by looking
 92 | ||| up its ID in the DOM. Unlike `getElementById`, this will throw
 93 | ||| an exception in the `JSIO` monad if the element is not found
 94 | ||| or can't be safely cast to the desired type.
 95 | export
 96 | getElementByRef : SafeCast t => ElemRef t -> JSIO t
 97 | getElementByRef (Id {tag} _ id) = strictGetElementById tag id
 98 | getElementByRef (Class _ class) = getElementByClass class
 99 | getElementByRef Body            = body
100 | getElementByRef Document        = document
101 | getElementByRef Window          = window
102 |
103 | err : String
104 | err = "Control.Monad.Dom.Interface.castElementByRef"
105 |
106 | ||| Tries to retrieve an element of the given type by looking
107 | ||| up its ID in the DOM. Unlike `getElementById`, this will throw
108 | ||| an exception in the `JSIO` monad if the element is not found
109 | ||| or can't be safely cast to the desired type.
110 | export
111 | castElementByRef : SafeCast t2 => ElemRef t -> JSIO t2
112 | castElementByRef (Id {tag} _ id) = strictGetElementById tag id
113 | castElementByRef (Class _ class) = getElementByClass class
114 | castElementByRef Body            = body >>= tryCast err
115 | castElementByRef Document        = document >>= tryCast err
116 | castElementByRef Window          = window >>= tryCast err
117 |