0 | module Web.MVC.Util
  1 |
  2 | import JS
  3 | import Text.CSS
  4 | import Text.HTML
  5 | import Web.Dom
  6 | import Web.Html
  7 | import Web.Raw.Geometry
  8 | import public Text.HTML.Ref
  9 | import public Text.HTML.Tag
 10 |
 11 | %default total
 12 |
 13 | ||| DOM type associacte with an ElemRef
 14 | public export
 15 | 0 ElemType : Ref t -> Type
 16 | ElemType (Id _)   = Element
 17 | ElemType (Elem _) = Element
 18 | ElemType Body     = HTMLElement
 19 | ElemType Document = Document
 20 | ElemType Window   = Window
 21 |
 22 | --------------------------------------------------------------------------------
 23 | --          Accessing and Updating Nodes
 24 | --------------------------------------------------------------------------------
 25 |
 26 | ||| Tries to retrieve an element of the given type by looking
 27 | ||| up its ID in the DOM. Unlike `getElementById`, this will throw
 28 | ||| an exception in the `JSIO` monad if the element is not found
 29 | ||| or can't be safely cast to the desired type.
 30 | export
 31 | strictGetElementById : SafeCast t => Maybe String -> (id : String) -> JSIO t
 32 | strictGetElementById mtag id = do
 33 |   Nothing <- castElementById t id | Just t => pure t
 34 |   liftJSIO $ throwError $
 35 |     let tag := fromMaybe "element" mtag
 36 |      in Caught "Web.MVC.Output.strictGetElementById: Could not find \{tag} with id \{id}"
 37 |
 38 | ||| Tries to retrieve a HTMLElement by looking
 39 | ||| up its ID in the DOM. Unlike `getElementById`, this will throw
 40 | ||| an exception in the `JSIO` monad if the element is not found
 41 | ||| or can't be safely cast to the desired type.
 42 | export %inline
 43 | strictGetHTMLElementById : (tag,id : String) -> JSIO HTMLElement
 44 | strictGetHTMLElementById = strictGetElementById . Just
 45 |
 46 | ||| Tries to retrieve an element of the given type by looking
 47 | ||| up its ID in the DOM. Unlike `getElementById`, this will throw
 48 | ||| an exception in the `JSIO` monad if the element is not found
 49 | ||| or can't be safely cast to the desired type.
 50 | export
 51 | getElementByRef : (r : Ref t) -> JSIO (ElemType r)
 52 | getElementByRef (Id {tag} id) = strictGetElementById (Just tag) id
 53 | getElementByRef (Elem id)     = strictGetElementById Nothing id
 54 | getElementByRef Body          = body
 55 | getElementByRef Document      = document
 56 | getElementByRef Window        = window
 57 |
 58 | err : String
 59 | err = "Web.MVC.Output.castElementByRef"
 60 |
 61 | ||| Tries to retrieve an element of the given type by looking
 62 | ||| up its ID in the DOM. Unlike `getElementById`, this will throw
 63 | ||| an exception in the `JSIO` monad if the element is not found
 64 | ||| or can't be safely cast to the desired type.
 65 | export
 66 | castElementByRef : {0 x : k} -> SafeCast t => Ref x -> JSIO t
 67 | castElementByRef (Id {tag} id) = strictGetElementById (Just tag) id
 68 | castElementByRef (Elem id)     = strictGetElementById Nothing id
 69 | castElementByRef Body          = body >>= tryCast err
 70 | castElementByRef Document      = document >>= tryCast err
 71 | castElementByRef Window        = window >>= tryCast err
 72 |
 73 | setVM : Ref t -> ValidityTag t -> String -> JSIO ()
 74 | setVM r SVButton s   = castElementByRef r >>= \x => HTMLButtonElement.setCustomValidity x s
 75 | setVM r SVFieldSet s = castElementByRef r >>= \x => HTMLFieldSetElement.setCustomValidity x s
 76 | setVM r SVInput s    = castElementByRef r >>= \x => HTMLInputElement.setCustomValidity x s
 77 | setVM r SVObject s   = castElementByRef r >>= \x => HTMLObjectElement.setCustomValidity x s
 78 | setVM r SVOutput s   = castElementByRef r >>= \x => HTMLOutputElement.setCustomValidity x s
 79 | setVM r SVSelect s   = castElementByRef r >>= \x => HTMLSelectElement.setCustomValidity x s
 80 | setVM r SVTextArea s = castElementByRef r >>= \x => HTMLTextAreaElement.setCustomValidity x s
 81 |
 82 | setVal : Ref t -> ValueTag t -> String -> JSIO ()
 83 | setVal r VButton s   = castElementByRef r >>= (HTMLButtonElement.value =. s)
 84 | setVal r VData s     = castElementByRef r >>= (HTMLDataElement.value =. s)
 85 | setVal r VInput s    = castElementByRef r >>= (HTMLInputElement.value =. s)
 86 | setVal r VOption s   = castElementByRef r >>= (HTMLOptionElement.value =. s)
 87 | setVal r VOutput s   = castElementByRef r >>= (HTMLOutputElement.value =. s)
 88 | setVal r VParam s    = castElementByRef r >>= (HTMLParamElement.value =. s)
 89 | setVal r VSelect s   = castElementByRef r >>= (HTMLSelectElement.value =. s)
 90 | setVal r VTextArea s = castElementByRef r >>= (HTMLTextAreaElement.value =. s)
 91 |
 92 | export
 93 | setValidityMessage : Ref t -> ValidityTag t => String -> JSIO ()
 94 | setValidityMessage r = setVM r %search
 95 |
 96 | export
 97 | setValue : Ref t -> ValueTag t => String -> JSIO ()
 98 | setValue r = setVal r %search
 99 |
100 | --------------------------------------------------------------------------------
101 | --          DOM Updates
102 | --------------------------------------------------------------------------------
103 |
104 | nodeList : DocumentFragment -> List (HSum [Node,String])
105 | nodeList df = [inject $ df :> Node]
106 |
107 | ||| Replaces all children of the given node with a new document fragment.
108 | export %inline
109 | replaceChildren : Element -> DocumentFragment -> JSIO ()
110 | replaceChildren elem = replaceChildren elem . nodeList
111 |
112 | ||| Appends the given document fragment to a DOM element's children
113 | export %inline
114 | appendDF : Element -> DocumentFragment -> JSIO ()
115 | appendDF elem = append elem . nodeList
116 |
117 | ||| Prepends the given document fragment to a DOM element's children
118 | export %inline
119 | prependDF : Element -> DocumentFragment -> JSIO ()
120 | prependDF elem = prepend elem . nodeList
121 |
122 | ||| Inserts the given document fragment after a DOM element.
123 | export %inline
124 | afterDF : Element -> DocumentFragment -> JSIO ()
125 | afterDF elem = after elem . nodeList
126 |
127 | ||| Inserts the given document fragment before a DOM element.
128 | export %inline
129 | beforeDF : Element -> DocumentFragment -> JSIO ()
130 | beforeDF elem = before elem . nodeList
131 |
132 | ||| Inserts the given document fragment before a DOM element.
133 | export %inline
134 | replaceDF : Element -> DocumentFragment -> JSIO ()
135 | replaceDF elem = replaceWith elem . nodeList
136 |
137 | --------------------------------------------------------------------------------
138 | --          Element Geometry
139 | --------------------------------------------------------------------------------
140 |
141 | export
142 | toRect : DOMRect -> JSIO Rect
143 | toRect r =
144 |   [| MkRect
145 |        (DOMRectReadOnly.x r)
146 |        (DOMRectReadOnly.y r)
147 |        (DOMRectReadOnly.height r)
148 |        (DOMRectReadOnly.width r)
149 |        (DOMRectReadOnly.top r)
150 |        (DOMRectReadOnly.bottom r)
151 |        (DOMRectReadOnly.left r)
152 |        (DOMRectReadOnly.right r)
153 |   |]
154 |
155 | export
156 | boundingRect : {0 x : k} -> Ref x -> JSIO Rect
157 | boundingRect ref = do
158 |   el <- castElementByRef {t = Element} ref
159 |   r  <- Element.getBoundingClientRect el
160 |   toRect r
161 |