Web.MVC.Controller.List

Definitions

data ListEv : Type -> Type

  An event fired when editing a list of items

Totality: total
Visibility: public export
Constructors:

Add : ListEv e

Del : Nat -> ListEv e

Change : Nat -> e -> ListEv e

0 ListEditor : Type -> Type -> Type -> Type -> Type

  Type alias for editors of lists.

Totality: total
Visibility: public export

0 List1Editor : Type -> Type -> Type -> Type -> Type

  Type alias for editors of lists.

Totality: total
Visibility: public export

data ListMode : Type

  Whether to append or prepend items added to the list

Totality: total
Visibility: public export
Constructors:

Append : ListMode

Prepend : ListMode

record ListEnv : Type -> Type

  Environment for setting up the UI elements

Totality: total
Visibility: public export
Constructor: 

LI : (i -> Nat -> i) -> (i -> i) -> Class -> (e -> Node e) -> (e -> Node e) -> ListMode -> ListEnv i

Projections:

.addIcon : ListEnv i -> e -> Node e

  Icon used for adding a row

.cls : ListEnv i -> Class

  Class suffix

.delIcon : ListEnv i -> e -> Node e

  Icon used for deleting a row

.listID : ListEnv i -> i -> i

  ID for the whole list base on a parent ID

.mode : ListEnv i -> ListMode

  Whether to append or prepend new values

.rowID : ListEnv i -> i -> Nat -> i

  ID for a single row

.rowID : ListEnv i -> i -> Nat -> i

  ID for a single row

Totality: total
Visibility: public export

rowID : ListEnv i -> i -> Nat -> i

  ID for a single row

Totality: total
Visibility: public export

.listID : ListEnv i -> i -> i

  ID for the whole list base on a parent ID

Totality: total
Visibility: public export

listID : ListEnv i -> i -> i

  ID for the whole list base on a parent ID

Totality: total
Visibility: public export

.cls : ListEnv i -> Class

  Class suffix

Totality: total
Visibility: public export

cls : ListEnv i -> Class

  Class suffix

Totality: total
Visibility: public export

.delIcon : ListEnv i -> e -> Node e

  Icon used for deleting a row

Totality: total
Visibility: public export

delIcon : ListEnv i -> e -> Node e

  Icon used for deleting a row

Totality: total
Visibility: public export

.addIcon : ListEnv i -> e -> Node e

  Icon used for adding a row

Totality: total
Visibility: public export

addIcon : ListEnv i -> e -> Node e

  Icon used for adding a row

Totality: total
Visibility: public export

.mode : ListEnv i -> ListMode

  Whether to append or prepend new values

Totality: total
Visibility: public export

mode : ListEnv i -> ListMode

  Whether to append or prepend new values

Totality: total
Visibility: public export

listRow : Cast i DomID => ListEnv i -> (i -> s -> Node e) -> i -> (Nat, s) -> Node (ListEv e)

  Row for editing a single value in a list of values.

Totality: total
Visibility: export

values : Cast i DomID => ListEnv i -> (i -> s -> Node e) -> i -> List (Nat, s) -> Node (ListEv e)

  A widget used for editing lists of values, using another
  widget for each individual value.

Totality: total
Visibility: export

list : Cast i DomID => ListEnv i -> Editor i s e t -> ListEditor i s e t

  An editor for lists of values, where values can be dynamically
  added or removed.

Totality: total
Visibility: export

list1 : Cast i DomID => ListEnv i -> String -> Editor i s e t -> List1Editor i s e t

Totality: total
Visibility: export