Web.MVC.Util

Reexports

import public Text.HTML.Ref
import public Text.HTML.Tag

Definitions

0 ElemType : Ref t -> Type

  DOM type associacte with an ElemRef

Totality: total
Visibility: public export

strictGetElementById : SafeCast t => Maybe String -> String -> JSIO t

  Tries to retrieve an element of the given type by looking
  up its ID in the DOM. Unlike `getElementById`, this will throw
  an exception in the `JSIO` monad if the element is not found
  or can't be safely cast to the desired type.

Totality: total
Visibility: export

strictGetHTMLElementById : String -> String -> JSIO HTMLElement

  Tries to retrieve a HTMLElement by looking
  up its ID in the DOM. Unlike `getElementById`, this will throw
  an exception in the `JSIO` monad if the element is not found
  or can't be safely cast to the desired type.

Totality: total
Visibility: export

getElementByRef : (r : Ref t) -> JSIO (ElemType r)

  Tries to retrieve an element of the given type by looking
  up its ID in the DOM. Unlike `getElementById`, this will throw
  an exception in the `JSIO` monad if the element is not found
  or can't be safely cast to the desired type.

Totality: total
Visibility: export

castElementByRef : SafeCast t => Ref x -> JSIO t

  Tries to retrieve an element of the given type by looking
  up its ID in the DOM. Unlike `getElementById`, this will throw
  an exception in the `JSIO` monad if the element is not found
  or can't be safely cast to the desired type.

Totality: total
Visibility: export

setValidityMessage : Ref t -> ValidityTag t => String -> JSIO ()

Totality: total
Visibility: export

setValue : Ref t -> ValueTag t => String -> JSIO ()

Totality: total
Visibility: export

replaceChildren : Element -> DocumentFragment -> JSIO ()

  Replaces all children of the given node with a new document fragment.

Totality: total
Visibility: export

appendDF : Element -> DocumentFragment -> JSIO ()

  Appends the given document fragment to a DOM element's children

Totality: total
Visibility: export

prependDF : Element -> DocumentFragment -> JSIO ()

  Prepends the given document fragment to a DOM element's children

Totality: total
Visibility: export

afterDF : Element -> DocumentFragment -> JSIO ()

  Inserts the given document fragment after a DOM element.

Totality: total
Visibility: export

beforeDF : Element -> DocumentFragment -> JSIO ()

  Inserts the given document fragment before a DOM element.

Totality: total
Visibility: export

replaceDF : Element -> DocumentFragment -> JSIO ()

  Inserts the given document fragment before a DOM element.

Totality: total
Visibility: export

toRect : DOMRect -> JSIO Rect

Totality: total
Visibility: export

boundingRect : Ref x -> JSIO Rect

Totality: total
Visibility: export