Text.HTML.Select

Definitions

data SelectEntry : Type -> Type

Totality: total
Visibility: public export
Constructors:

Title : String -> SelectEntry t

Entry : t -> String -> SelectEntry t

record SelectEv : Type -> Type

Totality: total
Visibility: public export
Constructor: 

SE : Nat -> String -> t -> SelectEv t

Projections:

.index : SelectEv t -> Nat

.label : SelectEv t -> String

.value : SelectEv t -> t

Hint: 

Functor SelectEv

.index : SelectEv t -> Nat

Totality: total
Visibility: public export

index : SelectEv t -> Nat

Totality: total
Visibility: public export

.label : SelectEv t -> String

Totality: total
Visibility: public export

label : SelectEv t -> String

Totality: total
Visibility: public export

.value : SelectEv t -> t

Totality: total
Visibility: public export

value : SelectEv t -> t

Totality: total
Visibility: public export

selectEntries : Sink (SelectEv e) => List (SelectEntry t) -> (t -> Bool) -> (t -> e) -> List (Attribute Select) -> HTMLNode

Totality: total
Visibility: export

selectFromListBy : Sink (SelectEv e) => List t -> (t -> Bool) -> (t -> String) -> (t -> e) -> List (Attribute Select) -> HTMLNode

  Create a `<select>` element displaying the options in the given
  list.
  
  @values  : the list of options
  @sel     : true if the given item in the list should be selected
  @display : how to display an option at the UI
  @toEvent : how to convert an option to an event
  @attrs   : additional attributes

Totality: total
Visibility: export

selectFromList : Sink (SelectEv e) => Eq t => List t -> Maybe t -> (t -> String) -> (t -> e) -> List (Attribute Select) -> HTMLNode

  Like `selectFromListBy` but uses an optional initial value
  to determine the initially selected value.
  
  @values  : the list of options
  @init    : the initially selected option (if any)
  @display : how to display an option at the UI
  @toEvent : how to convert an option to an event
  @attrs   : additional attributes

Totality: total
Visibility: export

selectEntries' : Sink e => List (SelectEntry t) -> (t -> Bool) -> (t -> e) -> List (Attribute Select) -> HTMLNode

  Simplified version of `selectEntries` that does not take
  a full `SelectEvent` sink.

Totality: total
Visibility: export

selectFromListBy' : Sink e => List t -> (t -> Bool) -> (t -> String) -> (t -> e) -> List (Attribute Select) -> HTMLNode

  Simplified version of `selectFromListBy` that does not take
  a full `SelectEvent` sink.

Totality: total
Visibility: export

selectFromList' : Sink e => Eq t => List t -> Maybe t -> (t -> String) -> (t -> e) -> List (Attribute Select) -> HTMLNode

  Simplified version of `selectFromList` that does not take
  a full `SelectEvent` sink.

Totality: total
Visibility: export