Text.HTML.DomID

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 -> HTMLNode -> HTMLNode

  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

  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

  `id` attribute for a DOM element

Totality: total
Visibility: export

uniqueID : LIO io => io DomID

  Generates a unique ID to be used to identify a DOM element.

Totality: total
Visibility: export

uniqueRef : LIO io => (0 t : HTMLTag s) -> io (Ref t)

  Uses `uniqueID` to generate a reference for a DOM element.

Totality: total
Visibility: export