Idris2Doc : Text.HTML.DomID

Text.HTML.DomID

(source)

Definitions

record DomID : Type
  Utility data type for accessing elements in the DOM.

This will improve type safety and give clearer semantics to a string
that is to be used as an identifier in the DOM.

Totality: total
Visibility: public export
Constructor: 
D : String -> DomID

Projection: 
.value : DomID -> String

Hints:
Cast Nat DomID
Cast x DomID => Cast (SnocList x) DomID
Cast x DomID => Cast (List x) DomID
All (\x => Cast (f x) DomID) ks => Cast (All f ks) DomID
Eq DomID
FromString DomID
Interpolation DomID
Ord DomID
Semigroup DomID
Show DomID
.value : DomID -> String
Totality: total
Visibility: public export
value : DomID -> String
Totality: total
Visibility: public export
toID : Cast t DomID => t -> DomID
  Alias for `cast` with better type inference.

Totality: total
Visibility: export
withDomID : Cast t DomID => t -> Node e -> Node e
  Specialized version of `withId` (which sets the `id` attribute of a
node) for working with `DomID`s.

Totality: total
Visibility: export
forID : Cast t DomID => t -> Attribute x e
  Set the `for` attribute of a DOM label to the given ID.

Totality: total
Visibility: export
tagRef : (0 tag : HTMLTag s) -> Cast t DomID => t -> Ref tag
Totality: total
Visibility: export
elemRef : Cast t DomID => t -> Ref Void
Totality: total
Visibility: export
btnRef : Cast t DomID => t -> Ref Button
  Identifier for accessing a `<button>` element

Totality: total
Visibility: export
divRef : Cast t DomID => t -> Ref Div
  Identifier for accessing a `<div>` element

Totality: total
Visibility: export
inpRef : Cast t DomID => t -> Ref Input
  Identifier for accessing an `<input>` element

Totality: total
Visibility: export
canvasRef : Cast t DomID => t -> Ref Canvas
  Identifier for accessing a `<canvas>` element

Totality: total
Visibility: export
ref : Cast t DomID => t -> Attribute tag e
  `id` attribute for a DOM element

Totality: total
Visibility: export