Rhone.JS.ElemRef

Definitions

data ElemRef : Type -> Type

  A typed reference to an element or container in the DOM. Elements can
  either be referenced by their ID string or their CSS class
  (both of which must be unique), or by holding a value directly.
  This can be used to access the element in question,
  for instance by invoking `getElementByRef`.
  
  In addition, we provide (pseudo-)element references for
  `body`, `document`, and `window`.

Totality: total
Visibility: public export
Constructors:

Id : (0 _ : ElementType tag t) -> String -> ElemRef t

Class : (0 _ : ElementType tag t) -> String -> ElemRef t

Body : ElemRef HTMLElement

Document : ElemRef Document

Window : ElemRef Window

data ById : ElemRef t -> Type

  Predicate witnessing that a given `ElemRef` is a reference
  by ID.

Totality: total
Visibility: public export
Constructor: 

IsById : ById (Id tpe id)

data ByClass : ElemRef t -> Type

  Predicate witnessing that a given `ElemRef` is a reference
  by Class.

Totality: total
Visibility: public export
Constructor: 

IsByClass : ByClass (Class tpe id)

ref : (r : ElemRef t) -> {auto 0 _ : ById r} -> Attribute ev

  Uses an element ref as an ID attribute

Totality: total
Visibility: export

idRef : (r : ElemRef t) -> {auto 0 _ : ById r} -> List Declaration -> Rule n

  Uses an element ref as an ID selector

Totality: total
Visibility: export

classRef : (r : ElemRef t) -> {auto 0 _ : ByClass r} -> List Declaration -> Rule n

  Uses an element ref as a class selector

Totality: total
Visibility: export

strictGetElementById : SafeCast t => 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 : SafeCast t => ElemRef t -> 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

castElementByRef : SafeCast t2 => ElemRef t -> JSIO t2

  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